1,721,087 research outputs found
Information flow analysis for fail-secure devices
Information security devices must preserve security properties even in the presence of faults. This in turn requires a rigorous evaluation of the system behaviours resulting from component failures, especially how such failures affect information flow. We introduce a compositional method of static analysis for fail-secure behaviour. Our method uses reachability matrices to identify potentially undesirable information flows based on the fault modes of the system's components
Relative Simulation and Model Checking of Real-Time Processes
Simulation and model checking are commonly used to compare the\ud
behaviour of a computer-based system with its requirements\ud
specification. However, when upgrading an operational legacy system\ud
the challenge is usually to compare the behaviour of a proposed new\ud
system against an old trusted one. Doing this for time-sensitive\ud
control systems is awkward because the behaviour of the system is\ud
dependent on that of its physical environment. Consequently, the old\ud
and new systems can be compared meaningfully only when they are\ud
simulated under exactly the same conditions. In this paper we show\ud
how this can be done by simulating both the old and new systems\ud
simultaneously, with both system models linked to the same environment\ud
model. The resulting simulation traces and model checking\ud
counterexamples allow the behaviours of a legacy real-time system and\ud
its proposed replacement to be compared directly and easily
Proceedings of the 21st Australian Software Engineering Conference (ASWEC 2010) : 6-9 April 2010, Auckland, New Zealand.
ASWEC is a joint conference of Engineers Australia and the Australian Computer Society reporting through the Engineers Australia/ACS Joint Board on Software Engineering
On the Efficacy of Prerecorded Lectures for Teaching Introductory Programming
Teaching introductory programming is a notoriously challenging problem\ud
in any information technology or computer science course. Failure and\ud
dropout rates are usually high, and many students seem unable to grasp\ud
the notion of solving problems algorithmically. Given contemporary\ud
students' fondness for multimedia styles of presentation, we conducted\ud
an experiment on the effectiveness of providing prerecorded\ud
mini-lectures in a first-year programming subject. Although we found\ud
only a weak quantitative correlation between students' use of the\ud
prerecorded material and their final grades, anecdotal feedback on the\ud
experiment was overwhelmingly positive, suggesting that students'\ud
perceptions of the subject were improved
Tracing secure information flow through mode changes
Communications devices intended for use in security-critical applications must be rigorously evaluated to ensure they preserve data confidentiality. This process includes tracing the flow of classified information through the device's circuitry. Previous work has shown how this can be done using graph analysis techniques for each of the device's distinct operating modes. However, such analyses overlook potential information flow between modes, via components that store information in one mode and release it in another. Here we show how\ud
graph-based analyses can be extended to allow for information flow through sequences of consecutive modes
Identifying Critical Components During Information Security Evaluations
Electronic communications devices intended for government or military applications must be rigorously evaluated to ensure that they maintain data confidentiality. High-grade information security evaluations require a detailed analysis of the device’s design, to determine how it achieves necessary security functions. In practice, such evaluations are labour-intensive and costly, so there is a strong incentive to find ways to make the process more efficient. In this paper we show how well-known concepts from graph theory can be applied to a device’s design to optimise information security evaluations. In particular, we use end-to-end graph traversals to eliminate components that do not need to be evaluated at all, and minimal cutsets to identify the smallest group of components that needs to be evaluated in depth
Functional analysis of a real-time protocol for networked control systems
Traditional real-time control systems are tightly integrated into the industrial processes they govern. Now, however, there is increasing interest in networked control systems. These provide greater flexibility and cost savings by allowing real-time controllers to interact with industrial processes over existing communications networks. New data packet queuing protocols are currently being developed to enable precise real-time control over a network with variable propagation delays. We show how one such protocol was formally modelled using timed automata, and how model checking was used to reveal subtle aspects of the control system's dynamic behaviour
Fault evaluation for security-critical communications devices
Computer communications devices intended for government or military applications must be carefully evaluated to ensure that they maintain data confidentiality even in the presence of component failures. Of particular concern is the need to identify so-called silent and complicit failures. In this article we present a structured technique for evaluating a device's logical design and physical construction to reveal potential fault modes. The approach combines information flow and risk analysis techniques to produce a thorough and transparent security argument
A hardware virtualization-based component sandboxing architecture
Modern applications comprise multiple components, such as browser plug-ins, often of unknown provenance and quality. Statistics show that failure of such components accounts for a high percentage of software faults. Enabling isolation of such fine-grained components is therefore necessary to increase the robustness and resilience of security-critical and safety-critical computer systems.\ud
In this paper, we evaluate whether such fine-grained components can be sandboxed through the use of the hardware virtualization support available in modern Intel and AMD processors. We compare the performance and functionality of such an approach to two previous software based approaches. The results demonstrate that hardware isolation minimizes the difficulties encountered with software based approaches, while also reducing the size of the trusted computing base, thus increasing confidence in the solution's correctness. We also show that our relatively simple implementation has equivalent run-time performance, with overheads of less than 34%, does not require custom tool chains and provides enhanced functionality over software-only approaches, confirming that hardware virtualization technology is a viable mechanism for fine-grained component isolation
- …
