The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.01 - January (2008 vol.34)
pp: 82-98
ABSTRACT
A major problem in verifying the security of code is that the code's large size makes it much too costly to verify in its entirety. This article describes a novel and practical approach to verifying the security of code which substantially reduces the cost of verification. In this approach, the security property of interest is represented formally and a compact security model, containing only information needed to reason about the policy, is constructed. To reduce the cost of verification, the code to be verified is partitioned into three categories: Only the first category, less than 10% of the code, requires requires substantial effort to verify; the proof of the other two categories is relatively trivial. Our approach was developed to support a Common Criteria evaluation of the separation kernel of an embedded software system. This article describes 1) our techniques and theory for verifying the kernel code and 2) the artifacts produced: a Top Level Specification (TLS), a formal statement of the security property, a mechanized proof that the TLS satisfies the property, the partitioning of the code, and a demonstration that the code conforms to the TLS. The article also presents the formal argument that the kernel code conforms to the TLS and consequently satisfies the security property.
INDEX TERMS
Specification, security, verification, security kernels, tools, Formal methods, Software, software verification
CITATION
Constance Heitmeyer, Myla Archer, Elizabeth Leonard, John McLean, "Applying Formal Methods to a Certifiably Secure Software System", IEEE Transactions on Software Engineering, vol.34, no. 1, pp. 82-98, January 2008, doi:10.1109/TSE.2007.70772
REFERENCES
[1] J.S. Moore, T.W. Lynch, and M. Kaufmann, “A Mechanically Checked Proof of the AMD5K86TM Floating-Point Division Program,” IEEE Trans. Computers, vol. 47, no. 9, Sept. 1998.
[2] J. Rushby, “A Formally Verified Algorithm for Clock Synchronization under a Hybrid Fault Model,” Proc. 13th ACM Symp. Principles of Distributed Computing, Aug. 1994.
[3] C. Meadows, “Analysis of the Internet Key Exchange Protocol Using the NRL Protocol Analyzer,” Proc. IEEE Symp. Security and Privacy, 1999.
[4] J. Juerjens, “Sound Methods and Effective Tools for Model-Based Security Engineering with UML,” Proc. 27th Int'l Conf. Software Eng., 2005.
[5] T. Benzel, “Analysis of a Kernel Verification,” Proc. IEEE Symp. Security and Privacy, Apr. 1984.
[6] R. Whitehurst and T. Lunt, “The SeaView Verification,” Proc. Second IEEE Computer Security Foundations Workshop, June 1989.
[7] J. Rushby, “Design and Verification of Secure Systems,” Proc. Eighth ACM Symp. Operating System Principles, Dec. 1981.
[8] B. Lampson, “Protection,” Proc. Fifth Princeton Conf. Information Sciences and Systems, Mar. 1991.
[9] N. Shankar, S. Owre, J.M. Rushby, and D.W.J. Stringer-Calvert, “PVS Prover Guide Version 2.4,” technical report, Computer Science Laboratory, SRI Int'l, Nov. 2001.
[10] M. Abadi and L. Lamport, “The Existence of Refinement Mappings,” Theoretical Computer Science, vol. 82, no. 2, pp. 253-284, 1991.
[11] C. Adams, “Keeping Secrets in Integrated Avionics,” Aviation Today, 2004.
[12] J. Anderson, “Computer Security Technology Planning Study,” Technical Report ESD-TR-73-51, Hanscom AFB, ESD/AFSC, 1972.
[13] “Common Criteria for Information Technology Security Evaluation,” Parts 1-3: Technical Reports CCIMB-2004-01-001 through CCIMB-2004-01-003, Version 2.2, Revision 256, Jan. 2004.
[14] C.E. Landwehr, C.L. Heitmeyer, and J.D. McLean, “A Security Model for Military Message Systems,” ACM Trans. Computer Systems, vol. 2, no. 3, pp. 198-222, 1984.
[15] J. McLean, C. Landwehr, and C. Heitmeyer, “A Formal Statement of the Military Message System Security Model,” Proc. IEEE Symp. Security and Privacy, pp. 188-194, 1984.
[16] M. Archer, “TAME: Using PVS Strategies for Special-Purpose Theorem Proving,” Annals of Math. and Artificial Intelligence, vol. 29, nos. 1-4, pp. 139-181, 2000.
[17] M. Archer, C.L. Heitmeyer, and E. Riccobene, “Proving Invariants of I/O Automata with TAME,” Automated Software Eng., vol. 9, no. 3, pp. 201-232, 2002.
[18] S. Owre, J. Rushby, N. Shankar, and F. von Henke, “Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS,” IEEE Trans. Software Eng., vol. 21, no. 2, pp. 107-125, Feb. 1995.
[19] Xcode Version 2.1, http://developer.apple.com/tools/xcode index.html , 2007.
[20] E.M. Clarke, O. Grumberg, and D.E. Long, “Model Checking and Abstraction,” Proc. 21st ACM Symp. Principles of Programming Language, 1994.
[21] K.L. McMillan, “Verification of Infinite State Systems by Compositional Model Checking,” Proc. 10th IFIP WG 10.5 Advanced Research Working Conf. Correct Hardware Design and Verification Methods, 1999.
[22] E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, “Counterexample-Guided Abstraction Refinement,” Proc. 12th Int'l Conf. Computer-Aided Verification, 2000.
[23] J.R. Burch and D.L. Dill, “Automatic Verification of Pipelined Microprocessors Control,” Proc. Sixth Int'l Conf. Computer-Aided Verification, vol. 818, pp. 68-80, 1994.
[24] D. Cyrluk, “Microprocessor Verification in PVS: A Methodology and Simple Example,” Technical Report SRI-CSL-93-12, 1993.
[25] L. Robinson and K.N. Levitt, “Proof Techniques for Hierarchically Structured Programs,” Comm. ACM, vol. 20, no. 4, pp. 271-283, 1977.
[26] B. Alpern and F.B. Schneider, “Defining Liveness,” Information Processing Letters, vol. 21, no. 4, pp. 181-185, 1985.
[27] L. Lamport, “Proving the Correctness of Multiprocess Programs,” IEEE Trans. Software Eng., vol. 3, no. 2, pp. 125-143, 1977.
[28] J. McLean, “A General Theory of Composition for Trace Sets Closed under Selective Interleaving Functions,” Proc. IEEE Symp. Research in Security and Privacy '94, pp. 79-93, May 1994.
[29] J.A. Goguen and J. Meseguer, “Security Policies and Security Models,” Proc. IEEE Symp. Research in Security and Privacy '92, pp.11-20, May 1992.
[30] J. McLean, “Security Models,” Encyclopedia of Software Eng., J.Marciniak, ed., John Wiley & Sons, 1994.
[31] F.B. Schneider, “Enforceable Security Policies,” ACM Trans. Information and System Security, vol. 3, no. 1, pp. 30-50, 2000.
[32] C.L. Heitmeyer, R.D. Jeffords, and B.G. Labaw, “Automated Consistency Checking of Requirements Specifications,” ACM Trans. Software Eng. and Methodology, vol. 5, no. 3, pp. 231-261, 1996.
[33] C.L. Heitmeyer, M. Archer, R. Bharadwaj, and R.D. Jeffords, “Tools for Constructing Requirements Specifications: The SCR Toolset at the Age of Ten,” Computer Systems: Science and Eng., vol. 20, no. 1, 2005.
[34] D. Greve, M. Wilding, and W.M. Vanfleet, “A Separation Kernel Formal Security Policy,” Proc. Fourth Int'l Workshop ACL2 Prover and Its Applications, July 2003.
[35] B. Meyer, “Applying 'Design by Contract',” Computer, vol. 25, no. 10, pp. 40-51, Oct. 1992.
[36] M. Chechik and J.D. Gannon, “Automatic Analysis of Consistency between Requirements and Designs,” IEEE Trans. Software Eng., vol. 27, no. 7, pp. 651-672, 2001.
[37] J. Barnes, High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley, 2003.
[38] M. Das, “Formal Specifications on Industrial-Strength Code: From Myth to Reality,” Proc. 18th Int'l Conf. Computer-Aided Verification, Aug. 2006.
[39] S. Hallem, B. Chelf, Y. Xie, and D.R. Engler, “A System and Language for Building System-Specific, Static Analyses,” Proc. ACM Conf. Programming Language Design and Implementation, pp.69-82, 2002.
[40] T. Kremenek, P. Twohey, G. Back, A. Ng, and D. Engler, “From Uncertainty to Belief: Inferring the Specification Within,” Proc. Seventh Symp. Operating Systems Design and Implementation, Dec. 2006.
[41] A. Gargantini and C.L. Heitmeyer, “Using Model Checking to Generate Tests from Requirements Specifications,” Proc. Seventh European Software Eng. Conf. and Seventh ACM Symp. Foundations of Software Eng., 1999.
[42] Y. Smaragdakis and C. Csallner, “Combining Static and Dynamic Reasoning for Bug Detection,” Proc. First Int'l Conf. Tests and Proofs, pp. 1-16, 2007.
[43] SCADE Tool Suite, http://www.esterel-technologies.com/ products scade-suite, 2007.
[44] T. Rothamel, C. Heitmeyer, E. Leonard, and Y.A. Liu, “Generating Optimized Code from SCR Specifications,” Proc. ACM Conf. Languages, Compilers and Tools for Embedded Systems, June 2006.
[45] L. Fraim, “Secure Office Management System: The First Commodity Application on a Trusted System,” Proc. Fall Joint Computer Conf. Exploring Technology: Today and Tomorrow, 1987.
[46] T. Lunt, D. Denning, R. Schell, M. Heckman, and W. Shockley, “The SeaView Security Model,” IEEE Trans. Software Eng., vol. 16, no. 6, pp. 593-607, June 1990.
[47] R. Smith, “Cost Profile of a Highly Assured Secure Operating System,” ACM Trans. Information and System Security, vol. 4, no. 1, Feb. 2001.
[48] S. Gerhart, D. Craigen, and T. Ralston, “Case Study: Multinet Gateway System,” IEEE Software, pp. 37-39, 1994.
[49] L. Robinson, “The HDM Handbook, Vol. 1: The Foundations of HDM,” SRI Project 4828, technical report, SRI Int'l, 1979.
[50] J. Rushby, F. von Henke, and S. Owre, “An Introduction to Formal Specification and Verification Using EHDM,” Technical Report CSL-91-2, SRI Int'l, Feb. 1991.
[51] D. Good, “Mechanical Proofs about Computer Programs,” Math. Logic and Programming Languages, C. Hoare and J. Shepherdson, eds., pp. 55-75, Prentice Hall, 1985.
[52] M. Archer and E. Leonard, “Establishing High Confidence in Code Implementations of Algorithms Using Formal Verification of Pseudo-Code,” Proc. Third Int'l Verification Workshop, 2006.
[53] J. Alves-Foss and C. Taylor, “An Analysis of the GWV Security Policy,” Proc. Fifth Int'l Workshop ACL2 Prover and Its Applications, 2004.
[54] D. Greve, R. Richards, and M. Wilding, “A Summary of Intrinsic Partitioning Verification,” Proc. Fifth Int'l Workshop ACL2 Prover and Its Applications, 2004.
[55] R. Richards, D. Greve, M. Wilding, and W. Vanfleet, “The Common Criteria, Formal Methods and ACL2,” Proc. Fifth Int'l Workshop ACL2 Prover and Its Applications, 2004.
[56] C. Heitmeyer, M. Archer, E. Leonard, and J. McLean, “Formal Specification and Verification of Data Separation in a Separation Kernel for an Embedded System,” Proc. 13th ACM Conf. Computer and Comm. Security, Oct.-Nov. 2006.
49 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool