research-article

Free access

Safe to the last instruction: automated verification of a type-safe operating system

Authors:

Jean Yang,

Chris HawblitzelAuthors Info & Claims

Communications of the ACM, Volume 54, Issue 12

Pages 123 - 131

https://doi.org/10.1145/2043174.2043197

Published: 01 December 2011 Publication History

All formats PDF

References

[1]

Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M. Boogie: A modular reusable verifier for object-oriented programs. In Formal Methods for Components and Objects (FMCO) (Amsterdam, the Netherlands, 2006), volume 4111.

Digital Library

Google Scholar

[2]

Bevier, W.R., Hunt Jr., W.A., Moore, J.S., Young, W.D. An approach to systems verification. J. Autom. Reason. 5, 4 (1989), 411--428.

Digital Library

Google Scholar

[3]

Chen, J., Hawblitzel, C., Perry, F., Emmi, M., Condit, J., Coetzee, D., Pratikakis, P. Type-preserving compilation for large-scale optimizing object-oriented compilers. SIGPLAN Not. 43, 6 (2008), 183--192.

Digital Library

Google Scholar

[4]

de Moura, L.M., Bjørner, N. Z3: An efficient SMT solver. In TACAS (2008), 337--340.

Digital Library

Google Scholar

[5]

Feng, X., Shao, Z., Dong, Y., Guo, Y. Certifying low-level programs with hardware interrupts and preemptive threads. In PLDI (2008), 170--182.

Digital Library

Google Scholar

[6]

Ford, B., Hibler, M., Lepreau, J., McGrath, R., Tullmann, P. Interface and execution models in the Fluke kernel. In OSDI (1999), 101--115.

Digital Library

Google Scholar

[7]

Hawblitzel, C., Petrank, E. Automated verification of practical garbage collectors. In POPL (2009), 441--453.

Digital Library

Google Scholar

[8]

Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe et al. seL4: Formal verification of an OS kernel. In Proceedings of the 22nd ACM Symposium on Operating Systems Principles (SOSP) (Big Sky, MT, Oct. 2009), ACM, 207--220.

Digital Library

Google Scholar

[9]

Liedtke, J., Elphinstone, K., Schönberg, S., Härtig, H., Heiser, G., Islam, N., Jaeger, T. Achieved IPC performance (still the foundation for extensibility). In Proceedings of the 6th Workshop on Hot Topics in Operating Systems (HotOS-VI) (Cape Cod, MA, May 5--6, 1997).

Digital Library

Google Scholar

[10]

McCreight, A., Shao, Z., Lin, C., Li, L. A general framework for certifying garbage collectors and their mutators. In PLDI (2007), 468--479.

Digital Library

Google Scholar

[11]

Morrisett, G., Walker, D., Crary, K., Glew, N. From System F to typed assembly language. In POPL '98: 25th ACM Symposium on Principles of Programming Languages (Jan. 1998), 85--97.

Digital Library

Google Scholar

[12]

Turing, A. Checking a large routine. In The Early British Computer Conferences, MIT Press, Cambridge, MA, 1989, 70--72.

Digital Library

Google Scholar

Cited By

View all

Erata FDeng SZaghloul FXiong WDemir OSzefer J(2023)Survey of Approaches and Techniques for Security Verification of Computer SystemsACM Journal on Emerging Technologies in Computing Systems10.1145/356478519:1(1-34)Online publication date: 19-Jan-2023
https://dl.acm.org/doi/10.1145/3564785
Vasudevan AManiatis PMartins R(2020)überSparkACM SIGOPS Operating Systems Review10.1145/3421473.342147654:1(8-22)Online publication date: 31-Aug-2020
https://dl.acm.org/doi/10.1145/3421473.3421476
Clarke EHenzinger TVeith H(2018)Introduction to Model CheckingHandbook of Model Checking10.1007/978-3-319-10575-8_1(1-26)Online publication date: 19-May-2018
https://doi.org/10.1007/978-3-319-10575-8_1
Show More Cited By

Index Terms

Safe to the last instruction: automated verification of a type-safe operating system

Recommendations

Safe to the last instruction: automated verification of a type-safe operating system
PLDI '10: Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation

Typed assembly language (TAL) and Hoare logic can verify the absence of many kinds of errors in low-level code. We use TAL and Hoare logic to achieve highly automated, static verification of the safety of a new operating system called Verve. Our ...
Safe to the last instruction: automated verification of a type-safe operating system
PLDI '10

Typed assembly language (TAL) and Hoare logic can verify the absence of many kinds of errors in low-level code. We use TAL and Hoare logic to achieve highly automated, static verification of the safety of a new operating system called Verve. Our ...
Automatic custom instruction identification for application-specific instruction set processors

The application-specific instruction set processors (ASIPs) have received more and more attention in recent years. ASIPs make trade-offs between flexibility and performance by extending the base instruction set of a general-purpose processor with custom ...

Comments

Information & Contributors

Information

Published In

Communications of the ACM Volume 54, Issue 12

December 2011

121 pages

ISSN:0001-0782

EISSN:1557-7317

DOI:10.1145/2043174

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 2011

Published in CACM Volume 54, 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

11
Total Citations
View Citations
17,644
Total Downloads

Downloads (Last 12 months)158
Downloads (Last 6 weeks)15

Reflects downloads up to 01 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Erata FDeng SZaghloul FXiong WDemir OSzefer J(2023)Survey of Approaches and Techniques for Security Verification of Computer SystemsACM Journal on Emerging Technologies in Computing Systems10.1145/356478519:1(1-34)Online publication date: 19-Jan-2023
Vasudevan AManiatis PMartins R(2020)überSparkACM SIGOPS Operating Systems Review10.1145/3421473.342147654:1(8-22)Online publication date: 31-Aug-2020
Clarke EHenzinger TVeith H(2018)Introduction to Model CheckingHandbook of Model Checking10.1007/978-3-319-10575-8_1(1-26)Online publication date: 19-May-2018
Amin NRompf T(2017)LMS-Verify: abstraction without regret for verified systems programmingACM SIGPLAN Notices10.1145/3093333.300986752:1(859-873)Online publication date: 1-Jan-2017
Amin NRompf TCastagna GGordon A(2017)LMS-Verify: abstraction without regret for verified systems programmingProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages10.1145/3009837.3009867(859-873)Online publication date: 1-Jan-2017
Castagna GGordon A(2017)Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming LanguagesundefinedOnline publication date: 1-Jan-2017
Asperti ARicciotti W(2015)A formalization of multi-tape Turing machinesTheoretical Computer Science10.1016/j.tcs.2015.07.013603:C(23-42)Online publication date: 25-Oct-2015
McGettrick A(2014)SpecificationComputing Handbook, Third Edition10.1201/b16812-101(1-8)Online publication date: 8-May-2014
Wang ZPu GLi JGu B(2012)A Type System for SPARDLProceedings of the 2012 Sixth International Symposium on Theoretical Aspects of Software Engineering10.1109/TASE.2012.47(209-216)Online publication date: 4-Jul-2012
Abadi M(2012)Software Security: A Formal PerspectiveFM 2012: Formal Methods10.1007/978-3-642-32759-9_1(1-5)Online publication date: 2012
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

Login options

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

References

Cited By

Index Terms

Recommendations