research-article

Empirical study towards a leading indicator for cost of formal software verification

Authors:

Daniel Matichuk,

June Andronick,

Mark StaplesAuthors Info & Claims

ICSE '15: Proceedings of the 37th International Conference on Software Engineering - Volume 1

Pages 722 - 732

Published: 16 May 2015 Publication History

Abstract

Formal verification can provide the highest degree of software assurance. Demand for it is growing, but there are still few projects that have successfully applied it to sizeable, real-world systems. This lack of experience makes it hard to predict the size, effort and duration of verification projects. In this paper, we aim to better understand possible leading indicators of proof size. We present an empirical analysis of proofs from the landmark formal verification of the seL4 microkernel and the two largest software verification proof developments in the Archive of Formal Proofs. Together, these comprise 15,018 individual lemmas and approximately 215,000 lines of proof script. We find a consistent quadratic relationship between the size of the formal statement of a property, and the final size of its formal proof in the interactive theorem prover Isabelle. Combined with our prior work, which has indicated that there is a strong linear relationship between proof effort and proof size, these results pave the way for effort estimation models to support the management of large-scale formal verification projects.

References

[1]

S. Checkoway, D. McCoy, B. Kantor, D. Anderson, H. Shacham, S. Savage, K. Koscher, A. Czeskis, F. Roesner, and T. Kohno, "Comprehensive experimental analyses of automotive attack surfaces," in Proceedings of the 20th USENIX Security Symposium, 2011.

Digital Library

[2]

D. Halperin, S. S. Clark, K. Fu, T. S. Heydt-Benjamin, B. Defend, T. Kohno, B. Ransford, W. Morgan, and W. H. Maisel, "Pacemakers and implantable cardiac defibrillators: Software radio attacks and zero-power defenses," in Proceedings of the IEEE Symposium on Security and Privacy, Oakland, CA, USA, May 2008, pp. 129--142.

Digital Library

[3]

K. Fisher, "HACMS: High assurance cyber military systems," in Proceedings of the 2012 ACM Conference on High Integrity Language Technology, ser. HILT '12. Boston, Massachusetts, USA: ACM, 2012, pp. 51--52.

Digital Library

[4]

(2012) Common criteria for information technology security evaluation, version 3.1 revision 4. {Online}. Available: http://www.commoncriteriaportal.org/cc/

[5]

Special Committee of RTCA, "DO-178C, software considerations in airborne systems and equipment certification," 2011.

[6]

X. Leroy, "Formal verification of a realistic compiler," Communications of the ACM, vol. 52, no. 7, pp. 107--115, 2009.

Digital Library

[7]

G. Klein, J. Andronick, K. Elphinstone, T. Murray, T. Sewell, R. Kolanski, and G. Heiser, "Comprehensive formal verification of an OS microkernel," ACM Transactions on Computer Systems, vol. 32, no. 1, pp. 2:1--2:70, Feb. 2014.

Digital Library

[8]

M. Staples, R. Kolanski, G. Klein, C. Lewis, J. Andronick, T. Murray, R. Jeffery, and L. Bass, "Formal specifications better than function points for code sizing," in International Conference on Software Engineering, David Notkin, Betty H. C. Cheng, Klaus Pohl, Ed. San Francisco, USA: IEEE, May 2013, Conference Paper, pp. 1257--1260.

Digital Library

[9]

R. Jeffery, M. Staples, J. Andronick, G. Klein, and T. Murray, "An empirical research agenda or understanding formal methods productivity," Information and Software Technology, 2015, to appear.

[10]

D. C. Stidolph and J. Whitehead, "Managerial issues for the consideration and use of formal methods," in In Stefania Gnesi, Keijiro Araki, and Dino Mandrioli (eds.), FME 2003, International Symposium of Formal Methods Europe, 2003, pp. 8--14.

[11]

M. Staples, R. Jeffery, J. Andronick, T. Murray, G. Klein, and R. Kolanski, "Productivity for proof engineering," in Empirical Software Engineering and Measurement, Turin, Italy, Sep. 2014, Conference Paper.

Digital Library

[12]

T. Nipkow, L. Paulson, and M. Wenzel, Isabelle/HOL --- A Proof Assistant for Higher-Order Logic, ser. Lecture Notes in Computer Science. Springer, 2002, vol. 2283.

Digital Library

[13]

G. Klein, T. Nipkow, and L. Paulson, "The archive of formal proofs," http://afp.sf.net, 2003.

[14]

M. Olszewska (Plska) and K. Sere, "Specification metrics for Event-B developments," in Proceedings of the CONQUEST 2010: "Software Quality Improvement", I. Schieferdecker, R. Seidl, and S. Goericke, Eds. International Software Quality Institute, 2010, p. 112.

[15]

M. H. Halstead, Elements of Software Science (Operating and Programming Systems Series). New York, NY, USA: Elsevier Science Inc., 1977.

Digital Library

[16]

Deploy: Industrial deployment of system engineering methods providing high dependability and productivity. {Online}. Available: http://www.deploy-project.eu/

[17]

W. B. Samson, D. G. Nevill, and P. I. Dugard, "Predictive software metrics based on a formal specification," Inf. Softw. Technol., vol. 29, no. 5, pp. 242--248, Jun. 1987.

Digital Library

[18]

T. McCabe, "A complexity measure," Software Engineering, IEEE Transactions on, vol. SE-2, no. 4, pp. 308--320, Dec 1976.

Digital Library

[19]

A. Tabareh, "Predictive Software Measures Based on Formal Z Specifications," Master's thesis, University of Gothenburg - Department of Computer Science and Engineering, 2011.

[20]

A. Bollin, "Metrics for quantifying evolutionary changes in Z specifications," Journal of Software: Evolution and Process, vol. 25, no. 9, pp. 1027--1059, 2013.

[21]

S. King, J. Hammond, R. Chapman, and A. Pryor, "Is proof more cost-effective than testing?" IEEE Trans. Softw. Eng., vol. 26, no. 8, pp. 675--686, Aug. 2000.

Digital Library

[22]

S. Berghofer and T. Nipkow, "Proof terms for simply typed higher order logic," in Theorem Proving in Higher Order Logics, ser. Lecture Notes in Computer Science, M. Aagaard and J. Harrison, Eds. Springer Berlin Heidelberg, 2000, vol. 1869, pp. 38--52.

Digital Library

[23]

S. Berghofer and M. Wenzel, "Inductive datatypes in HOL - lessons learned in formal-logic engineering," in Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics, ser. TPHOLs '99. London, UK, UK: Springer-Verlag, 1999, pp. 19--36.

Digital Library

[24]

T. Sewell, M. Myreen, and G. Klein, "Translation validation for a verified OS kernel," in ACM SIGPLAN Conference on Programming Language Design and Implementation. Seattle, Washington, USA: ACM, Jun. 2013, Conference Paper, pp. 471--481.

Digital Library

[25]

T. Sewell, S. Winwood, P. Gammie, T. Murray, J. Andronick, and G. Klein, "seL4 enforces integrity," in Proceedings of the 2nd International Conference on Interactive Theorem Proving, ser. Lecture Notes in Computer Science, M. C. J. D. van Eekelen, H. Geuvers, J. Schmaltz, and F. Wiedijk, Eds., vol. 6898. Nijmegen, The Netherlands: Springer, Aug. 2011, pp. 325--340.

Digital Library

[26]

T. Murray, D. Matichuk, M. Brassil, P. Gammie, T. Bourke, S. Seefried, C. Lewis, X. Gao, and G. Klein, "seL4: from general purpose to a proof of information flow enforcement," in IEEE Symposium on Security and Privacy, San Francisco, CA, May 2013, Conference Paper, pp. 415--429.

Digital Library

[27]

Trustworthy Systems Team, "seL4 proofs for API 1.03, release 2014-08-10," Aug 2014.

[28]

A. Lochbihler, "Jinja with threads," Archive of Formal Proofs, Dec. 2007, http://afp.sf.net/entries/JinjaThreads.shtml, Formal proof development.

[29]

F. Maric, "Formal verification of modern SAT solvers," Archive of Formal Proofs, Jul. 2008, http://afp.sf.net/entries/SATSolverVerification.shtml, Formal proof development.

[30]

D. Matichuk and T. Murray, "Extensible specifications for automatic re-use of specifications and proofs," in 10th International Conference on Software Engineering and Formal Methods, Thessaloniki, Greece, Dec. 2012, Conference Paper, p. 8.

Digital Library

[31]

D. Delahaye, "A tactic language for the system Coq," in International Conference on Logic for Programming, Artificial Intelligence and Reasoning, ser. Lecture Notes in Computer Science, vol. 1955. Springer, Nov. 2000.

Digital Library

[32]

D. Matichuk, M. Wenzel, and T. Murray, "An isabelle proof method language," in Interactive Theorem Proving (ITP), Vienna, Austria, Jul. 2014, Conference Paper, p. 16.

[33]

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions, ser. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004.

[34]

G. Grov, E. Komendantskaya, and A. Bundy, "A statistical relational learning challenge --- extracting proof strategies from exemplar proofs," in ICML12 Workshop on Statistical Relational Learning (SRL-2012), 2012.

[35]

E. Komendantskaya, J. Heras, and G. Grov, "Machine learning in proof general: Interfacing interfaces," in Proceedings 10th International Workshop On User Interfaces for Theorem Provers, UITP 2012, Bremen, Germany, July 11th, 2012., 2013, pp. 15--41.

[36]

D. Aspinall, "Proof general: A generic tool for proof development," in Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2000, pp. 38--43.

Digital Library

Cited By

Nagashima YHe YHuchard MKästner CFraser G(2018)PaMpeR: proof method recommendation system for Isabelle/HOLProceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering10.1145/3238147.3238210(362-372)Online publication date: 3-Sep-2018
https://dl.acm.org/doi/10.1145/3238147.3238210
Aspinall DKaliszyk C(2016)Towards Formal Proof MetricsProceedings of the 19th International Conference on Fundamental Approaches to Software Engineering - Volume 963310.1007/978-3-662-49665-7_19(325-341)Online publication date: 2-Apr-2016
https://dl.acm.org/doi/10.1007/978-3-662-49665-7_19
Blanchette JHaslbeck MMatichuk DNipkow T(2015)Mining the Archive of Formal ProofsProceedings of the International Conference on Intelligent Computer Mathematics - Volume 915010.1007/978-3-319-20615-8_1(3-17)Online publication date: 13-Jul-2015
https://dl.acm.org/doi/10.1007/978-3-319-20615-8_1

Index Terms

Empirical study towards a leading indicator for cost of formal software verification

Recommendations

Combining advanced formal hardware verification techniques
Formal Verification of Ada Programs

The Penelope verification editor and its formal basis are described. Penelope is a prototype system for the interactive development and verification of programs that are written in a rich subset of sequential Ada. Because it generates verification ...
Deductive software verification

Deductive software verification, also known as program proving, expresses the correctness of a program as a set of mathematical statements, called verification conditions. They are then discharged using either automated or interactive theorem provers. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICSE '15: Proceedings of the 37th International Conference on Software Engineering - Volume 1

May 2015

999 pages

ISBN:9781479919345

General Chair:
Antonia Bertolino
ISTI-CNR, Italy
,
Program Chairs:
Gerardo Canfora
University of Sannio, Italy
,
Sebastian Elbaum
University of Nebraska-Lincoln

Sponsors

ACM: Association for Computing Machinery
SIGSOFT: ACM Special Interest Group on Software Engineering
IEEE-CS\DATC: IEEE Computer Society
TCSE: IEEE Computer Society's Tech. Council on Software Engin.

Publisher

IEEE Press

Publication History

Published: 16 May 2015

Check for updates

Qualifiers

Research-article

Conference

ICSE '15

Sponsor:

ACM
SIGSOFT
IEEE-CS\DATC
TCSE

ICSE '15: 37th International Conference on Software Engineering

May 16 - 24, 2015

Florence, Italy

Acceptance Rates

Overall Acceptance Rate 276 of 1,856 submissions, 15%

Upcoming Conference

ICSE 2025

2025 IEEE/ACM 46th International Conference on Software Engineering

April 26 - May 3, 2025

Ottawa , ON , Canada

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
187
Total Downloads

Downloads (Last 12 months)5
Downloads (Last 6 weeks)0

Reflects downloads up to 22 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Nagashima YHe YHuchard MKästner CFraser G(2018)PaMpeR: proof method recommendation system for Isabelle/HOLProceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering10.1145/3238147.3238210(362-372)Online publication date: 3-Sep-2018
https://dl.acm.org/doi/10.1145/3238147.3238210
Aspinall DKaliszyk C(2016)Towards Formal Proof MetricsProceedings of the 19th International Conference on Fundamental Approaches to Software Engineering - Volume 963310.1007/978-3-662-49665-7_19(325-341)Online publication date: 2-Apr-2016
https://dl.acm.org/doi/10.1007/978-3-662-49665-7_19
Blanchette JHaslbeck MMatichuk DNipkow T(2015)Mining the Archive of Formal ProofsProceedings of the International Conference on Intelligent Computer Mathematics - Volume 915010.1007/978-3-319-20615-8_1(3-17)Online publication date: 13-Jul-2015
https://dl.acm.org/doi/10.1007/978-3-319-20615-8_1

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents