Abstract
In this paper we describe a novel yet practical approach to the formal verification of implementations. Our approach splits verification into two major parts. The first part verifies an implementation against a low-level specification written using source-code annotations. The second extracts a high-level specification from the implementation with the low-level specification, and proves that it implies the original system specification from which the system was built. Semantics-preserving refactorings are applied to the implementation in both parts to reduce the complexity of the verification. Much of the approach is automated. It reduces the verification burden by distributing it over separate tools and techniques, and it addresses both functional correctness and high-level properties at separate levels. As an illustration, we give a detailed example by verifying an optimized implementation of the Advanced Encryption Standard (AES) against its official specification.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)
Andronick, J., Chetali, B., Paulin-Mohring, C.: Formal Verification of Security Properties of Smart Card Embedded Source Code. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 302–317. Springer, Heidelberg (2005)
Barnes, J.: High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley, Reading (2003)
Bravenboer, M., Kalleberg, K.T., Vermaas, R., Visser, E.: Stratego/XT 0.16. A Language and Toolset for Program Transformation. Science of Computer Programming (2007)
Butler, R., Finnelli, G.: The Infeasibility of Quantifying the Reliability of Life-Critical Real-Time Software. IEEE Trans. on Software Engineering 19(1) (1993)
Chung, B., Gannod, G.C.: Abstraction of Formal Specifications from Program Code. In: IEEE 3rd Int. Conference on Tools for Artificial Intelligience, pp. 125–128 (1991)
Daemen, J., Rijmen, V.: AES Proposal: Rijndael. AES Algorithm Submission (1999)
Das, M.: Formal Specifications on Industrial Strength Code: From Myth to Reality. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144. Springer, Heidelberg (2006)
Das, M., Lerner, S., Seigle, M.: ESP: path-sensitive program verification in polynomial time. Programming Languages, Design and Implementation, pp. 57-68 (2002)
FIPS PUB 197, Advanced Encryption Standard. National Inst. of Standards & Tech. (2001)
Flanagan, C., Lieno, K.: Houdini, an annotation assistant for ESC/Java. Formal Methods Europe, Berlin, Germany (2001)
Floyd, R.W.: Assigning meanings to programs. In: Schwartz, J.T. (ed.) Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics 19 (American Mathematical Society), Providence, pp. 19–32 (1967)
Heitmeyer, C.L., Archer, M.M., Leonard, E.I., McLean, J.D.: Applying Formal Methods to a Certifiably Secure Software System. IEEE Trans. on Soft. Eng. 34(1) (2008)
Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2004)
Kataoka, Y., Ernst, M., Griswold, W., Notkin, D.: Automated support for program refactoring using invariants. In: Int. Conference on Software Maintenance, pp. 736–743 (2001)
Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer 7(3), 212–232 (2005)
Lerner, S.T., Millstein, E.R., Chambers, C.: Automated soundness proofs for dataflow analyses and transformations via local rules. Princ. of Prog. Lang., 364–377 (2005)
Liskov, B., Wing, J.: A Behavioral Notion of Subtyping. ACM Transactions on Programming Languages and Systems 16(6), 1811–1841 (1994)
National Institute of Standards Technology, The Common Criteria Evaluation and Validation Scheme, http://niap.nist.gov/cc-scheme/index.html
Runeson, J., Nystrom, S., Sjodin, J.: Optimizing code size through procedural abstraction. Languages, Compilers and Tools for Embedded Systems, pp. 204–215 (2000)
SCADE Suite, Esterel Technologies, http://www.esterel-technologies.com/
Strunk, E.A., Yin, X., Knight, J.C.: Echo: A Practical Approach to Formal Verification. In: FMICS 2005, Lisbon, Portugal (2005)
Ward, M.: Reverse Engineering through Formal Transformation. The Computer Journal 37(9), 795–813 (1994)
Weide, B.W.: Component-Based Systems. In: Marciniak, J.J. (ed.) Encyclopedia of Software Engineering. John Wiley and Sons, Chichester (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yin, X., Knight, J.C., Nguyen, E.A., Weimer, W. (2008). Formal Verification by Reverse Synthesis. In: Harrison, M.D., Sujan, MA. (eds) Computer Safety, Reliability, and Security. SAFECOMP 2008. Lecture Notes in Computer Science, vol 5219. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-87698-4_26
Download citation
DOI: https://doi.org/10.1007/978-3-540-87698-4_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-87697-7
Online ISBN: 978-3-540-87698-4
eBook Packages: Computer ScienceComputer Science (R0)