Skip to main content
SpringerLink
Log in

Correctness of Source-Level Safety Policies

  • Conference paper
  • First Online:
FME 2003: Formal Methods (FME 2003)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2805))

Included in the following conference series:

Abstract

Program certification techniques formally show that programs satisfy certain safety policies. They rely on the correctness of the safety policy which has to be established externally. In this paper we investigate an approach to show the correctness of safety policies which are formulated as a set of Hoare-style inference rules on the source code level. We develop a framework which is generic with respect to safety policies and which allows us to establish that proving the safety of a program statically guarantees dynamic safety, i.e., that the program never violates the safety property during its execution. We demonstrate our framework by proving safety policies for memory access safety and memory read/write limitations to be sound and complete. Finally, we formulate a set of generic safety inference rules which serve as the blueprint for the implementation of a verification condition generator which can be parameterized with different safety policies, and identify conditions on appropriate safety policies.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Amey, P., Chapman, R.: Industrial Strength Exception Freedom. In: 2002 SIGAda Intl. Conf. on Ada, pp. 1–9. ACM, New York (2002)

    Google Scholar 

  2. Appel, A.: Foundational proof-carrying code. In: LICS-16, pp. 247–258. IEEE, Los Alamitos (2001)

    Google Scholar 

  3. Foster, J.S., Fähndrich, M., Aiken, A.: A Theory of Type Qualifiers. In: PLDI, pp. 192–203. ACM, New York (1999)

    Chapter  Google Scholar 

  4. Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: PLDI, pp. 234–245. ACM, New York (2002)

    Google Scholar 

  5. Havelund, K., Roşu, G.: Monitoring Java Programs with Java PathExplorer. In: First Workshop on Runtime Verification. ENTCS, vol. 55(2). Elsevier, Amsterdam (2001)

    MATH  Google Scholar 

  6. Hamid, N.A., Shao, Z., Trifonov, V., Monnier, S., Ni, Z.: A Syntactic Approach to Foundational Proof-Carrying Code. In: LICS-17, pp. 89–100. IEEE, Los Alamitos (2002)

    Google Scholar 

  7. Kennedy, A.: Programming Languages and Dimensions. PhD thesis, University of Cambridge (April 1996)

    Google Scholar 

  8. Leino, K.R.M., Nelson, G.: An extended static checker for Modula-3. In: Koskimies, K. (ed.) CC 1998. LNCS, vol. 1383, pp. 302–305. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  9. Lowry, M., Pressburger, T., Rosu, G.: Certifying Domain-Specific Policies. In: 16th Intl. Conf. Automated Software Engineering, pp. 118–125. IEEE, Los Alamitos (2001)

    Google Scholar 

  10. League, C., Shao, Z., Trifonov, V.: Precision in Practice: A Type-Preserving Java Compiler. In: Hedin, G. (ed.) CC 2003. LNCS, vol. 2622, pp. 106–120. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  11. Mitchell, J.C.: Foundations for Programming Languages. The MIT Press, Cambridge (1996)

    Google Scholar 

  12. Necula, G.C., Lee, P.: The Design and Implementation of a Certifying Compiler. In: PLDI, pp. 333–344. ACM, New York (1998)

    Chapter  Google Scholar 

  13. Necula, G.C., Schneck, R.R.: A Gradual Approach to a More Trustworthy, yet Scalable, Proof-Carrying Code. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 47–62. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  14. PolySpace Technologies (2002), http://www.polyspace.com

  15. Reif, W.: The KIV Approach to Software Verification. In: Jähnichen, S., Broy, M. (eds.) KORSO 1995. LNCS, vol. 1009, pp. 339–370. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  16. Rittri, M.: Dimension Inference Under Polymorphic Recursion. In: 7th Conf. Functional Prog. Languages Computer Architecture, pp. 147–159. ACM, New York (1995)

    Google Scholar 

  17. Shankar, U., Talwar, K., Foster, J.S., Wagner, D.: Detecting Format String Vulnerabilities with Type Qualifiers. In: 10th Usenix Security Symposium (2001)

    Google Scholar 

  18. Walker, D.: A Type System for Expressive Security Policies. In: POPL-27, pp. 254–267. ACM, New York (2000)

    Google Scholar 

  19. Whalen, M., Schumann, J., Fischer, B.: Synthesizing Certified Code. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 431–450. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  20. Xi, H., Pfenning, F.: Eliminating Array Bound Checking Through Dependent Types. In: PLDI, pp. 249–257. ACM, New York (1998)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. QSS, NASA Ames Research Center, CA, 94035, Moffett Field, USA

    Ewen Denney

  2. RIACS, NASA Ames Research Center, CA, 94035, Moffett Field, USA

    Bernd Fischer

Authors
  1. Ewen Denney
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bernd Fischer
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Communication Engineering, Graduate School of Information Science and Electrical Engineering, Kyushu University, 6-10-1-Hakozaki, Higashi-ku, 812-8581, Fukuoka, Japan

    Keijiro Araki

  2. Istituto di Scienza e Tecnologie dell’Informazione “A. Faedo”, ISTI - CNR, Pisa, Italy

    Stefania Gnesi

  3. Dipartimento di Elettronica e Informazione, Politecnico di Milano, Italy

    Dino Mandrioli

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Denney, E., Fischer, B. (2003). Correctness of Source-Level Safety Policies. In: Araki, K., Gnesi, S., Mandrioli, D. (eds) FME 2003: Formal Methods. FME 2003. Lecture Notes in Computer Science, vol 2805. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45236-2_48

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-45236-2_48

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-40828-4

  • Online ISBN: 978-3-540-45236-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation