Formally-Based Security Evaluation Procedures

Contributors:

Colin Fidge, Luke Wildman, Tim McComb, Andrew Rae, Geoff Watson, Andrew Matthews, Scott Mallen and Gillian Day with students Yap Jin Hua, Yeo Puay Hong, Lim Soon Heng and Yu Sasaki

Description:

Government and military electronic communications networks rely on "domain-separation devices" to keep classified information secure. These include data diodes, encryption boxes, trusted filters and multi-computer switches. Guaranteeing that such devices are trustworthy is of vital national importance. Canberra's Defence Signals Directorate undertakes security evaluations for communications devices on both a commercial and "in-house" basis. These aim to prove that the device maintains data confidentiality in both normal operating modes and in the presence of component faults. This is done by examining the device in considerable detail, including its circuit design, embedded software and physical construction.

However, such evaluations are highly labour-intensive and hence costly. Therefore, this project aims to automate as much of the process as possible, in order to make security evaluations easier, more rigorous and repeatable. Achievements to date include:

Development of a new overall strategy for approaching security evaluations. This shows how a security argument can be structured as a combination of information-flow and fault-tree analyses.
Development of static analysis techniques for highlighting potential information flow through circuit diagrams. These include ways of identifying connectivity through the circuit in various operating modes, and ways of isolating those components of particular security interest.
Implementation of these techniques in an automated tool called the Secure Information Flow Analyser (SIFA). This allows circuit diagrams produced by the popular design tool Protel to be analysed for insecure information flows in a variety of ways.

Work to date has concentrated on device hardware, but attention is now turning to the embedded software running on microprocessor chips within the communications device itself. This is essential as security functions are now being increasingly delegated to software. Active areas of research include:

Developing ways of extending existing information flow analyses for secure software, which are mainly oriented towards application code such as operating systems, to embedded code which interacts directly with hardware.
Developing techniques and tools for translating embedded software into a form that can be integrated into the Secure Information Flow Analyser. This will allow information flow to be traced through both the hardware and software of a communications device.

SIFA:

SIFA (Secure Information Flow Analyser) uses a view-based approach to reason about the possible vulnerabilities of a system from an information security perspective. This includes both normal, intended operating modes and unintended operating states (in the presence of component or system-wide faults, for example). SIFA specialises in the analysis and evaluation of hardware devices, but is generic enough to support analysis over any interconnected structure of components.

Project Outputs:

B. W. Long, C. J. Fidge, and D. A. Carrington. Cross-layer verification of type flaw attacks on security protocols. In G. Dobbie, editor, Proceedings of the 30th Australasian Computer Science Conference (ACSC 2007), volume 62 of Conferences in Research and Practice in Information Technology, pages 171-180. Australian Computer Society, 2007.
A. J. Rae, C. J. Fidge, and L. P. Wildman. Fault evaluation for security-critical communications devices. IEEE Computer, 39(5):61-68, May 2006.
T.McComb and L. Wildman. Verifying Abstract Information Flow Properties in Fault Tolerant Security Devices In Eighth International Conference on Formal Engineering Methods (ICFEM 2006). LNCS 4260, pages 621--638, Springer, 2006.
B. W. Long and C. J. Fidge. Formally Analysing a Security Protocol for Replay Attacks. In J. Han and M. Staples, "Proceedings of the Australian Software Engineering Conference (ASWEC 2006)", pages 171-180. IEEE Computer Society Press, April 2006.
Fidge, C. and McComb, T. (2006). Tracing Information Flow Through Mode Changes <http://crpit.com/confpapers/CRPITV48Fidge.pdf>. In Proc. Twenty-Ninth Australasian Computer Science Conference (ACSC 2006), Hobart, Australia. CRPIT, 48. Estivill-Castro, V. and Dobbie, G., Eds., ACS. 303-310.
T. McComb and L. P. Wildman. SIFA: A tool for evaluation of high-grade security devices. ACISP 2005, 10th Australasian Conference on Information Security and Privacy, pp. 230 -- 241, Lecture Notes in Computer Science. Springer-Verlag, 2005.
B. Long. Formal verification of a type flaw attack on a security protocol Using Object-Z. ZB 2005: Formal Specification and Development in Z and B: 4th International Conference of B and Z Users, Guildford, UK, April 13-15, 2005, pg 319 LNCS 3455, 2005.
Graeme Smith and Luke Wildman. Model checking Z specifications using SAL. ZB 2005: Formal Specification and Development in Z and B: 4th International Conference of B and Z Users, Guildford, UK, April 13-15, 2005, pg 85 LNCS 3455, 2005.
A. J. Rae. Tracing security enforcing functions through communications devices. School of Information Technology and Electrical Engineering, The University of Queensland, November 2004.
A. J. Rae and C. J. Fidge. Information flow analysis for fail-secure devices. The Computer Journal, 48(1):17-26, January 2005. .
A. J. Rae and C. J. Fidge. Identifying critical components during information security evaluations. Journal of Research and Practice in Information Technology, 37(4):391-402, November 2005.
A. Matthews, S. Mallen and C. J. Fidge. Procedure for information security evaluations. Technical report, Defence Signals Directorate, February 2004. Version 1.1.
A. J. Rae and L. P. Wildman. A taxonomy of attacks on secure devices. In J. Slay, editor, Proceedings of the Fourth Australian Information Warfare and IT Security Conference, pages 251-263, November 2003.
B. Long. Formalising key distribution in the presence of trust using Object-Z. In C. Johnson, P. Montague, and C. Steketee, editors, Proc. Australasian Information Security Workshop (AISW 2003), volume 21 of Conferences in Research and Practice in Information Technology, pages 59-66. Australian Computer Society, 2003.
A. Cerone. Representing ASN.1 in Z. In C. Johnson, P. Montague, and C. Steketee, editors, Proc. Australasian Information Security Workshop (AISW 2003), volume 21 of Conferences in Research and Practice in Information Technology, pages 9-16. Australian Computer Society, 2003.
G. Smith. A formal framework for modelling and analysing mobile systems. In V. Estivill-Castro, editor, Twenty-Seventh Australasian Computer Science Conference (ACSC 2004), volume 26 of Conferences in Research and Practice in Information Technology, pages 193-202. Australian Computer Society, 2004.
C. J. Fidge. A survey of verification techniques for security protocols. Technical Report 01-22, Software Verification Research Centre, The University of Queensland, July 2001.

Funding:

This project is funded by the Defence Signals Directorate and the Australian Research Council.