skip to main content
research-article

From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification

Published: 14 January 2015 Publication History

Abstract

Many verifications of realistic software systems are monolithic, in the sense that they define single global invariants over complete system state. More modular proof techniques promise to support reuse of component proofs and even reduce the effort required to verify one concrete system, just as modularity simplifies standard software development. This paper reports on one case study applying modular proof techniques in the Coq proof assistant. To our knowledge, it is the first modular verification certifying a system that combines infrastructure with an application of interest to end users. We assume a nonblocking API for managing TCP networking streams, and on top of that we work our way up to certifying multithreaded, database-backed Web applications. Key verified components include a cooperative threading library and an implementation of a domain-specific language for XML processing. We have deployed our case-study system on mobile robots, where it interfaces with off-the-shelf components for sensing, actuation, and control.

Supplementary Material

MPG File (p609-sidebyside.mpg)

References

[1]
E. Alkassar, W. J. Paul, A. Starostin, and A. Tsyban. Pervasive verification of an OS microkernel: inline assembly, memory consumption, concurrent devices. In Proc. VSTTE, pages 71--85. Springer-Verlag, 2010.
[2]
A. W. Appel and D. McAllester. An indexed model of recursive types for foundational proof-carrying code. TOPLAS, 23(5):657--683, Sept. 2001.
[3]
H. Cai, Z. Shao, and A. Vaynberg. Certified self-modifying code. In Proc. PLDI, pages 66--77. ACM, 2007.
[4]
A. Chlipala. Mostly-automated verification of low-level programs in computational separation logic. In Proc.\ PLDI, pages 234--245. ACM, 2011.
[5]
A. Chlipala. The Bedrock structured programming system: Combining generative metaprogramming and Hoare logic in an extensible program verifier. In Proc.\ ICFP, pages 391--402. ACM, 2013.
[6]
A. Chlipala, G. Malecha, G. Morrisett, A. Shinnar, and R. Wisnesky. Effective interactive proofs for higher-order imperative programs. In Proc. ICFP, pages 79--90. ACM, 2009.
[7]
E. Cohen, M. Dahlweid, M. Hillebrand, D. Leinenbach, M. Moskal, T. Santen, W. Schulte, and S. Tobies. VCC: A practical system for verifying concurrent C. In Proc. TPHOLs, pages 23--42. Springer-Verlag, 2009.
[8]
M. Daum, N. W. Schirmer, and M. Schmidt. From operating-system correctness to pervasively verified applications. In Proc. IFM, pages 105--120. Springer-Verlag, 2010.
[9]
X. Feng and Z. Shao. Modular verification of concurrent assembly code with dynamic thread creation and termination. In Proc. ICFP, pages 254--267. ACM, 2005.
[10]
X. Feng, Z. Shao, Y. Dong, and Y. Guo. Certifying low-level programs with hardware interrupts and preemptive threads. In Proc. PLDI, pages 170--182. ACM, 2008.
[11]
X. Feng, Z. Shao, Y. Guo, and Y. Dong. Combining domain-specific and foundational logics to verify complete software systems. In Proc. VSTTE, pages 54--69. Springer-Verlag, 2008.
[12]
X. Feng, Z. Shao, A. Vaynberg, S. Xiang, and Z. Ni. Modular verification of assembly code with stack-based control abstractions. In Proc. PLDI, pages 401--414. ACM, 2006.
[13]
V. Gapeyev, M. Y. Levin, B. C. Pierce, and A. Schmitt. The Xtatic experience. In Proc. PLAN-X, 2005. University of Pennsylvania Technical Report MS-CIS-04--24, Oct 2004.
[14]
C. S. Gordon, M. D. Ernst, and D. Grossman. Rely-guarantee references for refinement types over aliased mutable data. In Proc. PLDI. ACM, 2013.
[15]
A. Gotsman, J. Berdine, B. Cook, N. Rinetzky, and M. Sagiv. Local reasoning for storable locks and threads. In Proc. APLAS, pages 19--37. Springer-Verlag, 2007.
[16]
A. Gotsman and H. Yang. Modular verification of preemptive OS kernels. In Proc. ICFP, pages 404--417. ACM, 2011.
[17]
A. Guha, M. Reitblatt, and N. Foster. Machine-verified network controllers. In Proc. PLDI, pages 483--494. ACM, 2013.
[18]
H. Hosoya and B. C. Pierce. XDuce: A statically typed XML processing language. ACM Transactions on Internet Technology, 3(2):117--148, May 2003.
[19]
C.-K. Hur and D. Dreyer. A Kripke logical relation between ML and assembly. In Proc. POPL, pages 133--146. ACM, 2011.
[20]
C. B. Jones. Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst., 5(4):596--619, Oct. 1983.
[21]
G. Klein. From a verified kernel towards verified systems. In Proc APLAS, pages 21--33. Springer-Verlag, 2010.
[22]
G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood. seL4: Formal verification of an OS kernel. In Proc. SOSP, pages 207--220. ACM, 2009.
[23]
X. Leroy. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In Proc. POPL, pages 42--54. ACM, 2006.
[24]
D. MacQueen. Modules for Standard ML. In Proc. LFP, pages 198--207. ACM, 1984.
[25]
G. Malecha, A. Chlipala, and T. Braibant. Compositional computational reflection. In Proc. ITP, pages 374--389. Springer-Verlag, 2014.
[26]
G. Malecha, G. Morrisett, A. Shinnar, and R. Wisnesky. Toward a verified relational database management system. In Proc. POPL, pages 237--248. ACM, 2010.
[27]
G. Malecha, G. Morrisett, and R. Wisnesky. Trace-based verification of imperative programs with I/O. J. Symb. Comput., 46(2):95--118, Feb. 2011.
[28]
A. McCreight, Z. Shao, C. Lin, and L. Li. A general framework for certifying garbage collectors and their mutators. In Proc. PLDI, pages 468--479. ACM, 2007.
[29]
Z. Ni and Z. Shao. Certified assembly programming with embedded code pointers. In Proc. POPL, pages 320--333. ACM, 2006.
[30]
Z. Ni, D. Yu, and Z. Shao. Using XCAP to certify realistic systems code: Machine context management. In Proc. TPHOLs, pages 189--206. Springer-Verlag, 2007.
[31]
F. Pottier. Hiding local state in direct style: A higher-order anti-frame rule. In Proc. LICS, pages 331--340. IEEE Computer Society, 2008.
[32]
M. Quigley, B. Gerkey, K. Conley, J. Faust, T. Foote, J. Leibs, E. Berger, R. Wheeler, and A. Ng. ROS: an open-source robot operating system. ICRA Workshop on Open Source Software, 2009.
[33]
J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In Proc. LICS, pages 55--74. IEEE Computer Society, 2002.
[34]
T. Streicher. Investigations into intensional type theory. Habilitation thesis, 1993.
[35]
K. Svendsen and L. Birkedal. Impredicative concurrent abstract predicates. In Proc. ESOP, pages 149--168. Springer-Verlag, 2014.
[36]
P. Wang, S. Cuellar, and A. Chlipala. Compiler verification meets cross-language linking via data abstraction. In Proc. OOPSLA, pages 675--690. ACM, 2014.
[37]
J. Yang and C. Hawblitzel. Safe to the last instruction: automated verification of a type-safe operating system. In Proc. PLDI, pages 99--110. ACM, 2010.

Cited By

View all
  • (2020)Separation logic for sequential programs (functional pearl)Proceedings of the ACM on Programming Languages10.1145/34089984:ICFP(1-34)Online publication date: 3-Aug-2020
  • (2016)A case for combining industrial pragmatics with formal methods2016 IEEE Cybersecurity Development (SecDev)10.1109/SecDev.2016.021(63-64)Online publication date: Nov-2016
  • (2016)Extensible and Efficient Automation Through Reflective TacticsProgramming Languages and Systems10.1007/978-3-662-49498-1_21(532-559)Online publication date: 2016
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices
ACM SIGPLAN Notices  Volume 50, Issue 1
POPL '15
January 2015
682 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2775051
  • Editor:
  • Andy Gill
Issue’s Table of Contents
  • cover image ACM Conferences
    POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
    January 2015
    716 pages
    ISBN:9781450333009
    DOI:10.1145/2676726
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 January 2015
Published in SIGPLAN Volume 50, Issue 1

Check for updates

Author Tags

  1. domain-specific languages
  2. internet servers
  3. modular program verification
  4. proof assistants
  5. thread libraries

Qualifiers

  • Research-article

Funding Sources

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)4
  • Downloads (Last 6 weeks)1
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2020)Separation logic for sequential programs (functional pearl)Proceedings of the ACM on Programming Languages10.1145/34089984:ICFP(1-34)Online publication date: 3-Aug-2020
  • (2016)A case for combining industrial pragmatics with formal methods2016 IEEE Cybersecurity Development (SecDev)10.1109/SecDev.2016.021(63-64)Online publication date: Nov-2016
  • (2016)Extensible and Efficient Automation Through Reflective TacticsProgramming Languages and Systems10.1007/978-3-662-49498-1_21(532-559)Online publication date: 2016
  • (2025)Generically Automating Separation Logic by Functors, Homomorphisms, and ModulesProceedings of the ACM on Programming Languages10.1145/37049039:POPL(1992-2024)Online publication date: 9-Jan-2025
  • (2022)Diaframe: automated verification of fine-grained concurrent programs in IrisProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523432(809-824)Online publication date: 9-Jun-2022
  • (2022)Resource Sharing for Verified High-Level Synthesis2022 IEEE 30th Annual International Symposium on Field-Programmable Custom Computing Machines (FCCM)10.1109/FCCM53951.2022.9786208(1-6)Online publication date: 15-May-2022
  • (2021)RefinedC: automating the foundational verification of C code with refined ownership typesProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454036(158-174)Online publication date: 19-Jun-2021
  • (2019)Scaling symbolic evaluation for automated verification of systems code with ServalProceedings of the 27th ACM Symposium on Operating Systems Principles10.1145/3341301.3359641(225-242)Online publication date: 27-Oct-2019
  • (2019)From C to interaction trees: specifying, verifying, and testing a networked serverProceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3293880.3294106(234-248)Online publication date: 14-Jan-2019
  • (2017)LMS-Verify: abstraction without regret for verified systems programmingACM SIGPLAN Notices10.1145/3093333.300986752:1(859-873)Online publication date: 1-Jan-2017
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media