Advertisement

Formal Verification by Reverse Synthesis

  • Xiang Yin
  • John C. Knight
  • Elisabeth A. Nguyen
  • Westley Weimer
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5219)

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.

Keywords

Formal verification formal methods software dependability 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)zbMATHGoogle Scholar
  2. 2.
    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)Google Scholar
  3. 3.
    Barnes, J.: High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley, Reading (2003)Google Scholar
  4. 4.
    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)Google Scholar
  5. 5.
    Butler, R., Finnelli, G.: The Infeasibility of Quantifying the Reliability of Life-Critical Real-Time Software. IEEE Trans. on Software Engineering 19(1) (1993)Google Scholar
  6. 6.
    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)Google Scholar
  7. 7.
    Daemen, J., Rijmen, V.: AES Proposal: Rijndael. AES Algorithm Submission (1999)Google Scholar
  8. 8.
    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)CrossRefGoogle Scholar
  9. 9.
    Das, M., Lerner, S., Seigle, M.: ESP: path-sensitive program verification in polynomial time. Programming Languages, Design and Implementation, pp. 57-68 (2002)Google Scholar
  10. 10.
    FIPS PUB 197, Advanced Encryption Standard. National Inst. of Standards & Tech. (2001)Google Scholar
  11. 11.
    Flanagan, C., Lieno, K.: Houdini, an annotation assistant for ESC/Java. Formal Methods Europe, Berlin, Germany (2001)Google Scholar
  12. 12.
    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)Google Scholar
  13. 13.
    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)Google Scholar
  14. 14.
    Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2004)Google Scholar
  15. 15.
    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)Google Scholar
  16. 16.
    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)CrossRefGoogle Scholar
  17. 17.
    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)Google Scholar
  18. 18.
    Liskov, B., Wing, J.: A Behavioral Notion of Subtyping. ACM Transactions on Programming Languages and Systems 16(6), 1811–1841 (1994)CrossRefGoogle Scholar
  19. 19.
    National Institute of Standards Technology, The Common Criteria Evaluation and Validation Scheme, http://niap.nist.gov/cc-scheme/index.html
  20. 20.
    Runeson, J., Nystrom, S., Sjodin, J.: Optimizing code size through procedural abstraction. Languages, Compilers and Tools for Embedded Systems, pp. 204–215 (2000)Google Scholar
  21. 21.
    SCADE Suite, Esterel Technologies, http://www.esterel-technologies.com/
  22. 22.
    Strunk, E.A., Yin, X., Knight, J.C.: Echo: A Practical Approach to Formal Verification. In: FMICS 2005, Lisbon, Portugal (2005)Google Scholar
  23. 23.
    Ward, M.: Reverse Engineering through Formal Transformation. The Computer Journal 37(9), 795–813 (1994)CrossRefGoogle Scholar
  24. 24.
    Weide, B.W.: Component-Based Systems. In: Marciniak, J.J. (ed.) Encyclopedia of Software Engineering. John Wiley and Sons, Chichester (2001)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Xiang Yin
    • 1
  • John C. Knight
    • 1
  • Elisabeth A. Nguyen
    • 2
  • Westley Weimer
    • 1
  1. 1.Department of Computer Science, CharlottesvilleUniversity of VirginiaVirginiaU.S.A.
  2. 2.Software Systems Engineering Department, ChantillyThe Aerospace CorporationVirginiaU.S.A.

Personalised recommendations