Zhong Shao
Abstract
Only if the programmer can prove (through formal machine-checkable proofs) it is free of bugs with respect to a claim of dependability.
- 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. Google Scholar
Digital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Hales, T. C. Formal proof. Notices of the AMS 55, 11 (Dec. 2008), 1370--1380.Google Scholar
- Hall, A. and Chapman, R. Correctness by construction: Developing a commercial secure system. IEEE Software 19, 1 (Jan./Feb. 2002), 18--25. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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
- Hoare, C. A. R. An axiomatic basis for computer programming. Commun. ACM 12, 10 (Oct. 1969), 576--580. Google ScholarDigital Library
- Huet, G., Paulin-Mohring, C., et al. The Coq Proof Assistant Reference Manual. The Coq Release v6.3.1, May 2000; http://coq.inria.frGoogle Scholar
- 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. Google ScholarDigital Library
- Jackson, D., Thomas, M., and Millett, L. Software for Dependable Systems: Sufficient Evidence? The National Academies Press, Washington, D.C., 2007. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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
- 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
- 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. Google ScholarDigital Library
- Thompson, K. Reflections on trusting trust. Commun. ACM 27, 8 (Aug. 1984), 761--763. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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/ Google ScholarDigital Library
Index Terms
- Certified software
Recommendations
Reviews
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