research-article

Free access

Certified software

Author:

Zhong ShaoAuthors Info & Claims

Communications of the ACM, Volume 53, Issue 12

Pages 56 - 66

https://doi.org/10.1145/1859204.1859226

Published: 01 December 2010 Publication History

All formats PDF

Abstract

Only if the programmer can prove (through formal machine-checkable proofs) it is free of bugs with respect to a claim of dependability.

References

[1]

Appel, A. W. Foundational proof-carrying code. In Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science (Boston, June 16--19). IEEE Press, Los Alamitos, CA, 2001, 247--258.

Digital Library

Google Scholar

[2]

Barendregt, H. P. and Geuvers, H. Proof-assistants using dependent type systems. In Handbook of Automated Reasoning, A. Robinson and A. Voronkov, Eds. Elsevier Scientific Publishing BV, Amsterdam, The Netherlands, 2001, 1149--1238.

Digital Library

Google Scholar

[3]

Cai, H., Shao, S., and Vaynberg, A. Certified self-modifying code. In Proceedings of the 2007 ACM Conference on Programming Language Design and Implementation (San Diego, June 10--13). ACM Press, New York, 2007, 66--77.

Digital Library

Google Scholar

[4]

Colby, C., Lee, P., Necula, G., Blau, F., Plesko, M., and Cline, K. A certifying compiler for Java. In Proceedings of the 2000 ACM Conference on Programming Language Design and Implementation (Vancouver, B.C., June 18--21). ACM press, New York, 2000, 95--107.

Digital Library

Google Scholar

[5]

DeMillo, R. A., Lipton, R. J., and Perlis, A. J. Social processes and proofs of theorems and programs. In Proceedings of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Los Angeles, Jan.17--19). ACM Press, New York, 1977, 206--214.

Digital Library

Google Scholar

[6]

de Moura, L. M. and Bjørner, N. Z3: An efficient SMT solver. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Vol. 4963 of LNCS) (Budapest, Mar. 29--Apr. 6). Springer-Verlag, Berlin, 2008, 337--340.

Digital Library

Google Scholar

[7]

Feng, X., Shao, Z., Guo, Y., and Dong, Y. Combining domain-specific and foundational logics to verify complete software systems. In Proceedings of the Second IFIP Working Conference on Verified Software: Theories, Tools, and Experiments (Vol. 5295 of LNCS) (Toronto, Oct. 6--9). Springer-Verlag, Berlin, 2008, 54--69.

Digital Library

Google Scholar

[8]

Feng, X., Shao, Z., Dong, Y., and Guo, Y. Certifying low-level programs with hardware interrupts and preemptive threads. In Proceedings of the 2008 ACM Conference on Programming Language Design and Implementation (Tucson, AZ, June 10--13). ACM Press, New York, 2008, 170--182.

Digital Library

Google Scholar

[9]

Feng, X., Ni, Z., Shao, Z., and Guo, Y. An open framework for foundational proof carrying code. In Proceedings of the 2007 ACM SIGPLAN International Workshop on Types in Language Design and Implementation (Nice, France, Jan. 16). ACM Press, New York, 2007, 67--78.

Digital Library

Google Scholar

[10]

Feng, X., Shao, Z., Vaynberg, A., Xiang, S., and Ni, Z. Modular verification of assembly code with stack-based control abstractions. In Proceedings of the 2006 ACM Conference on Programming Language Design and Implementation (Ottawa, June 11--14). ACM Press, New York, 2006, 401--414.

Digital Library

Google Scholar

[11]

Hales, T. C. Formal proof. Notices of the AMS 55, 11 (Dec. 2008), 1370--1380.

Google Scholar

[12]

Hall, A. and Chapman, R. Correctness by construction: Developing a commercial secure system. IEEE Software 19, 1 (Jan./Feb. 2002), 18--25.

Digital Library

Google Scholar

[13]

Hamid, N. A., Shao, Z., Trifonov, V., Monnier, S., and Ni, Z. A syntactic approach to foundational proof-carrying code. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (Copenhagen, July 22--25). IEEE Press, Los Alamitos, CA 2002, 89--100.

Digital Library

Google Scholar

[14]

Hoare, C. A. R. and Misra, J. Verified software: Theories, tools, experiments. In Proceedings of the First IFIP Working Conference on Verified Software: Theories, Tools, and Experiments (Vol. 4171 of LNCS) (Zurich, Oct. 10--13). Springer-Verlag, Berlin 2005, 1--18.

Google Scholar

[15]

Hoare, C. A. R. An axiomatic basis for computer programming. Commun. ACM 12, 10 (Oct. 1969), 576--580.

Digital Library

Google Scholar

[16]

Huet, G., Paulin-Mohring, C., et al. The Coq Proof Assistant Reference Manual. The Coq Release v6.3.1, May 2000; http://coq.inria.fr

Google Scholar

[17]

Ishtiaq, S. and O'Hearn, P. W. BI as an assertion language for mutable data structures. In Proceedings of the 28th ACM Symposium on Principles of Programming Languages (London, Jan. 17--19). ACM Press, New York, 2001, 14--26.

Digital Library

Google Scholar

[18]

Jackson, D., Thomas, M., and Millett, L. Software for Dependable Systems: Sufficient Evidence? The National Academies Press, Washington, D.C., 2007.

Digital Library

Google Scholar

[19]

King, S. T., Chen, P. M., Wang, Y.-M., Verbowski, C., Wang, H. J., and Lorch, J. Subvirt: Implementing malware with virtual machines. In Proceedings of the 2006 IEEE Symposium on Security and Privacy (Oakland, CA, May 21--24). IEEE Press, Los Alamitos, CA, 2006, 314--327.

Digital Library

Google Scholar

[20]

Leroy, X. Formal certification of a compiler back-end or: Programming a compiler with a proof assistant. In Proceedings of the 33rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Charleston, SC, Jan. 11--13). ACM Press, New York, 2006, 42--54.

Digital Library

Google Scholar

[21]

McCreight, A., Shao, Z., Lin, C., and Li, L. A general framework for certifying garbage collectors and their mutators. In Proceedings of the 2007 ACM Conference on Programming Language Design and Implementation (San Diego, June 10--13). ACM Press, New York, 2007, 468--479.

Digital Library

Google Scholar

[22]

Morrisett, G., Walker, D., Crary, K., and Glew, N. From System F to typed assembly language. In Proceedings of the 25th ACM Symposium on Principles of Programming Languages (San Diego, Jan. 19--21). ACM Press, New York, 1998, 85--97.

Digital Library

Google Scholar

[23]

Necula, G. and Lee, P. Safe kernel extensions without run-time checking. In Proceedings of the Second USENIX Symposium on Operating System Design and Implementation (Seattle, Oct. 28--31). USENIX Association, Berkeley, CA, 1996, 229--243.

Digital Library

Google Scholar

[24]

Ni, Z. and Shao, Z. Certified assembly programming with embedded code pointers. In Proceedings of the 33rd Symposium on Principles of Programming Languages (Charleston, SC, Jan. 11--13). ACM Press, New York, 2006, 320--333.

Digital Library

Google Scholar

[25]

O'Hearn, P. W. Resources, concurrency and local reasoning. In Proceedings of the 15th International Conference on Concurrency Theory (Vol. 3170 of LNCS) (London, Aug. 31--Sept. 3). Spinger-Verlag, Berlin, 2004, 49--67.

Google Scholar

[26]

Pnueli, A., Siegel, M., and Singerman, E. Translation validation. In Proceedings of the Fourth International Conference on Tools and Algorithms for Construction and Analysis of Systems (Vol. 1384 of LNCS) (Lisbon, Portugal, Mar. 28--Apr. 4). Springer-Verlag, Berlin 1998, 151--166.

Digital Library

Google Scholar

[27]

Reynolds, J. C. Separation logic: A logic for shared mutable data structures. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (Copenhagen, July 22--25). IEEE Press, Los Alamitos, CA 2002, 55--74.

Digital Library

Google Scholar

[28]

Schulte, W., Xia, S., Smans, J., and Piessens, F. A glimpse of a verifying C compiler. In Proceedings of the C/C++ Verification Workshop (Oxford, U.K., July 2, 2007).

Google Scholar

[29]

Shao, Z. An overview of the FLINT/ML compiler. In Proceedings of the ACM SIGPLAN Workshop on Types in Compilation (Amsterdam, The Netherlands, June 8, 1997).

Google Scholar

[30]

Tarditi, D., Morrisett, G., Cheng, P., Stone, C., Harper, R., and Lee, P. TIL: A type-directed optimizing compiler for ML. In Proceedings of the 1996 ACM Conference on Programming Language Design and Implementation (Philadelphia, May 21--24). ACM Press, New York, 1996, 181--192.

Digital Library

Google Scholar

[31]

Thompson, K. Reflections on trusting trust. Commun. ACM 27, 8 (Aug. 1984), 761--763.

Digital Library

Google Scholar

[32]

Yu, D., Hamid, N. A., and Shao, Z. Building certified libraries for PCC: Dynamic storage allocation. In Proceedings of the 2003 European Symposium on Programming (Vol. 2618 of LNCS) (Warsaw, Apr. 7--11). Springer-Verlag, Berlin, 2003, 363--379.

Digital Library

Google Scholar

[33]

Zeldovich, N. Securing Untrustworthy Software Using Information Flow Control. Ph.D. thesis, Department of Computer Science, Stanford University, Oct. 2007; http://www.cs.stanford.edu/histar/

Digital Library

Google Scholar

Cited By

View all

Qian ZSun GXing XDhiman G(2024)Refinement modeling and verification of secure operating systems for communication in digital twinsDigital Communications and Networks10.1016/j.dcan.2022.07.01210:2(304-314)Online publication date: Apr-2024
https://doi.org/10.1016/j.dcan.2022.07.012
Koenig J(2022)Grounding Game Semantics in Categorical AlgebraElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.372.26372(368-383)Online publication date: 3-Nov-2022
https://doi.org/10.4204/EPTCS.372.26
Oliveira Vale AMelliès PShao ZKoenig JStefanesco L(2022)Layered and object-based game semanticsProceedings of the ACM on Programming Languages10.1145/34987036:POPL(1-32)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498703
Show More Cited By

Index Terms

Recommendations

Reviews

Reviewer: Larry Bernstein

I am of two minds on this paper advocating formal machine-checkable proofs for software components. On one hand, Shao's survey of the state of the practice is disheartening. He reviews all of our frustrations with making software dependable. On the other hand, when he describes certified software on page 58, he explains what is possible within our current technology. He gives us hope without hype. I urge you to skip the first part, and start with the "What It Is" section on page 58. Then, you may go back to the beginning with a note of optimism. I fear that if you start at the beginning, you will stop reading and cry before you get to his important insights. I quibble with Shao's strict definition that our goal is to meet the specification. Software is supposed to solve the customer problem even when the specification is wrong. The heart of the matter is that we software engineers must produce safe, reliable, and secure software. When components meet these standards of quality, they are deemed trustworthy. Consequently, trustworthiness with respect to its initial specification may not be sufficient. As we discover flaws in the specification, we need to correct them. Shao points to ways to reduce the cost of producing specifications and proofs. His call for dynamic validation is welcome, and his description of recent advances is optimistic. For example, his observation that programmers need only to make sure that control is passed to the original return address is a welcome simplification in certifying software components. His call for the use of static analysis, that we must shape the software we write to fit the needs of such analyzers, is a thoughtful design constraint that Les Hatton [1] first called for, and that now fits into the dependable philosophy for software development. Shao cites that the challenge in building dependable systems "is to identify the right requirements and properties for verification." Since it is impossible to do this at the start, certification must become a continuing process through the incremental builds and specification corrections. This paper shows the way that such an approach is possible. Now, with a heavy heart, read his first few pages about the way things are actually done, and be inspired to make things better. We can follow Shao's lead and make our software-intensive systems trustworthy. Online Computing Reviews Service

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

Communications of the ACM Volume 53, Issue 12

December 2010

127 pages

ISSN:0001-0782

EISSN:1557-7317

DOI:10.1145/1859204

Issue’s Table of Contents

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 ACM 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: 01 December 2010

Published in CACM Volume 53, Issue 12

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Research-article
Popular
Refereed

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

33
Total Citations
View Citations
3,040
Total Downloads

Downloads (Last 12 months)360
Downloads (Last 6 weeks)44

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Qian ZSun GXing XDhiman G(2024)Refinement modeling and verification of secure operating systems for communication in digital twinsDigital Communications and Networks10.1016/j.dcan.2022.07.01210:2(304-314)Online publication date: Apr-2024
https://doi.org/10.1016/j.dcan.2022.07.012
Koenig J(2022)Grounding Game Semantics in Categorical AlgebraElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.372.26372(368-383)Online publication date: 3-Nov-2022
https://doi.org/10.4204/EPTCS.372.26
Oliveira Vale AMelliès PShao ZKoenig JStefanesco L(2022)Layered and object-based game semanticsProceedings of the ACM on Programming Languages10.1145/34987036:POPL(1-32)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498703
Koenig JShao ZHermanns HZhang LKobayashi NMiller D(2020)Refinement-Based Game Semantics for Certified Abstraction LayersProceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3373718.3394799(633-647)Online publication date: 8-Jul-2020
https://dl.acm.org/doi/10.1145/3373718.3394799
Karl HKundisch DMeyer auf der Heide FWehrheim H(2019)A Case for a New IT Ecosystem: On-The-Fly ComputingBusiness & Information Systems Engineering10.1007/s12599-019-00627-x62:6(467-481)Online publication date: 9-Dec-2019
https://doi.org/10.1007/s12599-019-00627-x
Barthe GBetarte GCampo JLuna C(2019)System-Level Non-interference of Constant-Time Cryptography. Part IJournal of Automated Reasoning10.1007/s10817-017-9441-563:1(1-51)Online publication date: 1-Jun-2019
https://dl.acm.org/doi/10.1007/s10817-017-9441-5
Shein E(2017)Hacker-proof codingCommunications of the ACM10.1145/310542360:8(12-14)Online publication date: 24-Jul-2017
https://dl.acm.org/doi/10.1145/3105423
Fu JLin YZhang X(2017)Impact of Environment on Branch Transfer of SoftwareSecurity and Privacy in Communication Networks10.1007/978-3-319-59608-2_32(575-593)Online publication date: 14-Jun-2017
https://doi.org/10.1007/978-3-319-59608-2_32
Gu RShao ZChen HWu XKim JSjöberg VCostanzo DKeeton KRoscoe T(2016)CertiKOSProceedings of the 12th USENIX conference on Operating Systems Design and Implementation10.5555/3026877.3026928(653-669)Online publication date: 2-Nov-2016
https://dl.acm.org/doi/10.5555/3026877.3026928
Cunha PSobrinho ÁDias da Silva LPerkusich AMiranda J(2016)Design of a Simulation Device to Test Electrogastrography (EGG) SystemsEncyclopedia of E-Health and Telemedicine10.4018/978-1-4666-9978-6.ch012(142-156)Online publication date: 2016
https://doi.org/10.4018/978-1-4666-9978-6.ch012
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Digital Edition

View this article in digital edition.

Digital Edition

Magazine Site

View this article on the magazine site (external)

Magazine Site

Get Access

Login options

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

Cited By

Index Terms

Recommendations

Certified software manager Secrets To Acing The Exam and Successful Finding And Landing Your Next Certified software manager Certified Job

Certified Software Product Manager (ISPMA) Secrets To Acing The Exam and Successful Finding And Landing Your Next Certified Software Product Manager (ISPMA) Certified Job

Certified Professional for Software Architecture (iSAQB) Secrets To Acing The Exam and Successful Finding And Landing Your Next Certified Professional for Software Architecture (iSAQB) Certified Job

Reviews

Access critical reviews of Computing literature here