| | This Article | |
| |
| |
| | Share | |
| |
| |
| | Bibliographic References | |
| |
| |
| | Add to: | |
| |
 Digg
 Furl
 Spurl
 Blink
 Simpy
 Google
 Del.icio.us
 Y!MyWeb
| |
| | Search | |
| |
| |
| | |
Applying Formal Methods to a Certifiably Secure Software System
January 2008 (vol. 34 no. 1)
pp. 82-98
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.
[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.
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, Jan. 2008, doi:10.1109/TSE.2007.70772
