Advertisement

Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems

  • Xinyu Feng
  • Zhong Shao
  • Yu Guo
  • Yuan Dong
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5295)

Abstract

A major challenge for verifying complete software systems is their complexity. A complete software system consists of program modules that use many language features and span different abstraction levels (e.g. user code and run-time system code). It is extremely difficult to use one verification system (e.g. type system or Hoare-style program logic) to support all these features and abstraction levels. In our previous work, we have developed a new methodology to solve this problem. We apply specialized “domain-specific” verification systems to verify individual program modules and then link the modules in a foundational open logical framework to compose the verified complete software package. In this paper, we show how this new methodology is applied to verify a software package containing implementations of preemptive threads and a set of synchronization primitives. Our experience shows that domain-specific verification systems can greatly simplify the verification process of low-level software, and new techniques for combining domain-specific and foundational logics are critical for the successful verification of complete software systems.

Keywords

Program Logic Assembly Code Separation Logic Interrupt Handler Code Pointer 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Bevier, W.R.: Kit: A study in operating system verification. IEEE Trans. Softw. Eng. 15(11), 1382–1396 (1989)CrossRefGoogle Scholar
  2. 2.
    Bevier, W.R., Hunt, W.A., Moore, J.S., Young, W.D.: Special issue on system verification. Journal of Automated Reasoning 5(4), 409–530 (1989)Google Scholar
  3. 3.
    Cai, H., Shao, Z., Vaynberg, A.: Certified self-modifying code. In: PLDI 2007, pp. 66–77 (June 2007)Google Scholar
  4. 4.
    Coq Development Team. The Coq proof assistant reference manual. The Coq release v8.1Google Scholar
  5. 5.
    Elphinstone, K., Klein, G., Derrin, P., Roscoe, T., Heiser, G.: Towards a practical, verified kernel. In: Proc. 11th Workshop on Hot Topics in Operating Systems (May 2007)Google Scholar
  6. 6.
    Feng, X., Ni, Z., Shao, Z., Guo, Y.: An open framework for foundational proof-carrying code. In: TLDI 2007, pp. 67–78 (January 2007)Google Scholar
  7. 7.
    Feng, X., Shao, Z., Dong, Y., Guo, Y.: Certifying low-level programs with hardware interrupts and preemptive threads. In: PLDI 2008 ( to appear, June 2008)Google Scholar
  8. 8.
    Feng, X., Shao, Z., Guo, Y., Dong, Y.: Combining domain-specific and foundational logics to verify complete software systems, extended version and Coq implementations (2008), http://flint.cs.yale.edu/flint/publications/itrimp.html
  9. 9.
    Feng, X., Shao, Z., Vaynberg, A., Xiang, S., Ni, Z.: Modular verification of assembly code with stack-based control abstractions. In: PLDI 2006, pp. 401–414 (June 2006)Google Scholar
  10. 10.
    Gargano, M., Hillebrand, M.A., Leinenbach, D., Paul, W.J.: On the correctness of operating system kernels. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603. Springer, Heidelberg (2005)Google Scholar
  11. 11.
    Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. on Programming Languages and Systems 5(4), 596–619 (1983)zbMATHCrossRefGoogle Scholar
  12. 12.
    McCreight, A., Shao, Z., Lin, C., Li, L.: A general framework for certifying garbage collectors and their mutators. In: PLDI 2007, pp. 468–479 (June 2007)Google Scholar
  13. 13.
    Ni, Z., Shao, Z.: Certified assembly programming with embedded code pointers. In: Proc. 33rd ACM Symp. on Principles of Prog. Lang, pp. 320–333 (2006)Google Scholar
  14. 14.
    Ni, Z., Yu, D., Shao, Z.: Using XCAP to certify realistic systems code: Machine context management. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 189–206. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  15. 15.
    O’Hearn, P.W.: Resources, concurrency and local reasoning. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 49–67. Springer, Heidelberg (2004)Google Scholar
  16. 16.
    O’Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: POPL 2004, pp. 268–280 (January 2004)Google Scholar
  17. 17.
    Paulin-Mohring, C.: Inductive definitions in the system Coq—rules and properties. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  18. 18.
    Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proc. LICS 2002, pp. 55–74 (July 2002)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Xinyu Feng
    • 1
  • Zhong Shao
    • 2
  • Yu Guo
    • 3
  • Yuan Dong
    • 4
  1. 1.Toyota Technological Institute at Chicago 
  2. 2.Yale University 
  3. 3.University of Science and Technology of China 
  4. 4.Tsinghua University 

Personalised recommendations