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.

Computerizing the welfare state: An international comparison of computerization in social security

Although computer technology is central to the operation of the modern welfare state, there has been little analysis of its role or of the factors shaping the way in which it is used. Using data generated by expert informants from 13 OECD countries, this paper provides an indicative comparison of the aims of computerization in national social security systems over a 15-year period from 1985 to 2000. The paper seeks to identify and explain patterns in the data and outlines and examines four hypotheses. Building on social constructivist accounts of technology, the first three hypotheses attribute variations in the aims of computerization to different welfare state regimes, forms of capitalism, and structures of public administration. The fourth hypothesis, which plays down the importance of social factors, assumes that computerization is adopted as a means of improving operational efficiency and generating expenditure savings. The findings suggest that, in all 13 countries, computerization was adopted in the expectation that it would lead to increased productivity and higher standards of performance, thus providing most support for the fourth hypothesis. However, variations between countries suggest that the sociopolitical values associated with different welfare state regimes have also had some effect in shaping the ways in which computer technology has been used in national social security systems.

Fault evaluation for security-critical communications devices

Communications devices for government or military applications must keep data secure, even when their electronic components fail. Combining information flow and risk analyses could make fault-mode evaluations for such devices more efficient and cost-effective.

SIFA: A tool for evaluation of high-grade security devices

We describe a tool for analysing information flow in security hardware. It identifies both sub-circuits critical to the preservation of security as well as the potential for information flow due to hardware failure. The tool allows for the composition of both logical and physical views of circuit designs. An example based on a cryptographic device is provided.

Verifying abstract information flow properties in fault tolerant security devices

The verification of information flow properties of security devices is difficult because it involves the analysis of schematic diagrams, artwork, embedded software, etc. In addition, a typical security device has many modes, partial information flow, and needs to be fault tolerant. We propose a new approach to the verification of such devices based upon checking abstract information flow properties expressed as graphs. This approach has been implemented in software, and successfully used to find possible paths of information flow through security devices.

A Z based approach to verifying security protocols

Security protocols preserve essential properties, such as confidentiality and authentication, of electronically transmitted data. However, such properties cannot be directly expressed or verified in contemporary formal methods. Via a detailed example, we describe the phases needed to formalise and verify the correctness of a security protocol in the state-oriented Z formalism.

Formal verification of type flaw attacks in security protocols

Security protocols are often modelled at a high level of abstraction, potentially overlooking implementation-dependent vulnerabilities. Here we use the Z specification language's rich set of data structures to formally model potentially ambiguous messages that may be exploited in a 'type flaw' attack. We then show how to formally verify whether or not such an attack is actually possible in a particular protocol using Z's schema calculus.