Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Software Security

ISSS 2002: Software Security — Theories and Systems pp 217–233Cite as

Formalization and Verification of a Mail Server in Coq

  • Conference paper
  • First Online:

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

Abstract

This paper reports on the formalization and verification of a mail server (SMTP server) in Coq. The correctness of a mail server is very important: bugs of the mail server may be abused for eavesdropping mail contents, spreading virus, sending spam messages, etc. We have verified a part of a mail server written in Java, by manually translating the Java program into a Coq function as faithfully as possible, and verifying properties of the Coq function. The results of this experiment indicate the feasibility and usefulness of verification of middle-sized system softwares in this style. The verification has been carried out in a few months, and a few bugs in the mail server have been indeed found during the verification process.

This is a preview of subscription content, 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   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. D. Bernstein and various contributors. The qmail home page. http://www.qmail.org.

  2. Y. Bertot. A certified compiler for an imperative language. Technical Report RR-3488, INRIA, Sep. 1998.

    Google Scholar 

  3. P. E. Black. Axiomatic Semantics Verification of a Secure Web Server. PhD thesis, Department of Computer Science, Brigham Young University, Feb. 1998.

    Google Scholar 

  4. P. E. Black and P. J. Windley. Inference rules for programming languages with side effects in expressions. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics, volume 1125 of Lecture Notes in Computer Science, pages 51–60. Springer-Verlag, August 1996.

    Google Scholar 

  5. E. M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. ACM ransactions on Programming Languages and Systems, 16(5):1512–1542, September 1994.

    Article  Google Scholar 

  6. E. M. Clarke and J. M. Wing. Formal methods: state of the art and future directions. ACM Computing Surveys, 28(4):626–643, 1996.

    Article  Google Scholar 

  7. F. B. Cohen. Why is thttpd secure? Available at http://www.all.net/journal/white/whitepaper.html.

  8. T. N. Dieter Nazareth. Formal verification of algorithm W: The monomorphic case. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics, volume 1125 of Lecture Notes in Computer Science, pages 331–345. Springer-Verlag, Aug. 1996.

    Google Scholar 

  9. B. Dutertre and S. Schneider. Using a PVS embedding of CSP to verify authentication protocols. In A. F. Elsa L. Gunter, editor, Theorem Proving in Higher Order Logics, volume 1275 of Lecture Notes in Computer Science, pages 121–136. Springer-Verlag, Aug. 1997.

    Chapter  Google Scholar 

  10. J.-C. Filliâtre. Preuve de programmes impératifs en théorie des types. PhD thesis, Université Paris-Sud, Jul. 1999. Available at http://www.lri.fr/~filliatr/ftp/publis/these.ps.gz.

  11. B. C. Pierce and J. Vouillon. Specifying a file synchronizer (full version). Draft, Mar. 2002.

    Google Scholar 

  12. J. B. Postel. Rfc 821: Simple mail transfer protocol. Available at http://www.faqs.org/rfcs/rfc821.html, Aug. 1982.

  13. E. Shibayama, S. Hagihara, N. Kobayashi, S. Nishizaki, K. Taura, and T. Watanabe. AnZenMail: A secure and certified e-mail system. In M. Okada, B. Pierce, A. Scedrov, H. Tokuda, and A. Yonezawa, editors, Proceedings of International Symposium on Software Security, Keio University, Tokyo, Japan (Nov. 2002), Lecture Notes in Computer Science. Springer-Verlag, Feb. 2003.

    Google Scholar 

  14. The Coq Development Team. The Coq proof assistant reference manual. Available at http://coq.inria.fr/doc/main.html, 2002.

  15. P. Wadler. Monads for functional programming. In M. Broy, editor, Marktoberdorf Summer School on Program Design Calculi, volume 118 of NATO ASI Series F: Computer and systems sciences. Springer-Verlag, Aug. 1992. Also in J. Jeuring and E. Meijer, editors, Advanced Functional Programming, Springer Verlag, LNCS 925, 1995. Some errata fixed August 2001.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Tokyo, Japan

    Reynald Affeldt

  2. Department of Computer Science, Tokyo Institute of Technology, Japan

    Naoki Kobayashi

Authors
  1. Reynald Affeldt
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Naoki Kobayashi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Keio University, 2-15-45 Mita, Minatoku, 108-8345, Tokyo, Japan

    Mitsuhiro Okada

  2. University of Pennsylvania, 200 South 33rd St., 19104, Philadelphia, PA, USA

    Benjamin C. Pierce

  3. University of Pennsylvania, 209 South 33rd St., 19104-6395, Philadelphia, PA, USA

    Andre Scedrov

  4. Keio University, 5322 Endoh, 252-8520, Fujisawa, Japan

    Hideyuki Tokuda

  5. University of Tokyo, 7-3-1 Hongo, Bunkyo-ku, 113, Tokyo, Japan

    Akinori Yonezawa

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Affeldt, R., Kobayashi, N. (2003). Formalization and Verification of a Mail Server in Coq. In: Okada, M., Pierce, B.C., Scedrov, A., Tokuda, H., Yonezawa, A. (eds) Software Security — Theories and Systems. ISSS 2002. Lecture Notes in Computer Science, vol 2609. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36532-X_14

Download citation

  • DOI: https://doi.org/10.1007/3-540-36532-X_14

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-00708-1

  • Online ISBN: 978-3-540-36532-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation