research-article

Verified compilation on a verified processor

Authors:

Anthony FoxAuthors Info & Claims

PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation

Pages 1041 - 1053

https://doi.org/10.1145/3314221.3314622

Published: 08 June 2019 Publication History

Get Access

Abstract

Developing technology for building verified stacks, i.e., computer systems with comprehensive proofs of correctness, is one way the science of programming languages furthers the computing discipline. While there have been successful projects verifying complex, realistic system components, including compilers (software) and processors (hardware), to date these verification efforts have not been compatible to the point of enabling a single end-to-end correctness theorem about running a verified compiler on a verified processor.

In this paper we show how to extend the trustworthy development methodology of the CakeML project, including its verified compiler, with a connection to verified hardware. Our hardware target is Silver, a verified proof-of-concept processor that we introduce here. The result is an approach to producing verified stacks that scales to proving correctness, at the hardware level, of the execution of realistic software including compilers and proof checkers. Alongside our hardware-level theorems, we demonstrate feasibility by hosting and running our verified artefacts on an FPGA board.

References

[1]

2018. IEEE Standard for System Verilog-Unified Hardware Design, Specification, and Verification Language. IEEE Std 1800-2017 (Revision of IEEE Std 1800-2012) (2018).

Google Scholar

[2]

Eyad Alkassar, Mark A. Hillebrand, Dirk Leinenbach, Norbert W. Schirmer, and Artem Starostin. 2008. The Verisoft Approach to Systems Verification. In Verified Software: Theories, Tools, Experiments (VSTTE).

Digital Library

Google Scholar

[3]

Andrew W. Appel, Lennart Beringer, Adam Chlipala, Benjamin C. Pierce, Zhong Shao, Stephanie Weirich, and Steve Zdancewic. 2017. Position paper: the science of deep specification. Philosophical Transactions of the Royal Society of London A: Mathematical, Physical and Engineering Sciences 375, 2104 (2017).

Google Scholar

[4]

William R. Bevier, Warren A. Hunt, J Strother Moore, and William D. Young. 1989. An approach to systems verification. Journal of Automated Reasoning 5, 4 (1989).

Digital Library

Google Scholar

[5]

Sven Beyer, Christian Jacobi, Daniel Kroening, and Dirk Leinenbach. 2002. Correct Hardware by Synthesis from PVS. Technical Report. http://www-wjp.cs.uni-sb.de/publikationen/BJKL02.pdf.

Google Scholar

[6]

Sven Beyer, Christian Jacobi, Daniel Kröning, Dirk Leinenbach, and Wolfgang J. Paul. 2006. Putting it all together - Formal verification of the VAMP. International Journal on Software Tools for Technology Transfer (STTT) 8, 4 (2006).

Digital Library

Google Scholar

Cited By

View all

Athalye ACorrigan-Gibbs HKaashoek FTassarotti JZeldovich NWitchel EArpaci-Dusseau ARossbach CKeeton K(2024)Modular Verification of Secure and Leakage-Free Systems: From Application Specification to Circuit-Level ImplementationProceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles10.1145/3694715.3695956(655-672)Online publication date: 4-Nov-2024
https://dl.acm.org/doi/10.1145/3694715.3695956
Erbsen APhilipoom JJamner DLin AGruetter SPit-Claudel CChlipala A(2024)Foundational Integration Verification of a Cryptographic ServerProceedings of the ACM on Programming Languages10.1145/36564468:PLDI(1704-1729)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656446
Gruetter SFukala VChlipala A(2024)Live Verification in an Interactive Proof AssistantProceedings of the ACM on Programming Languages10.1145/36564398:PLDI(1535-1558)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656439
Show More Cited By

Index Terms

Verified compilation on a verified processor
1. Hardware
  1. Electronic design automation
    1. Hardware description languages and compilation
  2. Hardware validation
    1. Functional verification
      1. Theorem proving and SAT solving
2. Software and its engineering
  1. Software notations and tools
    1. Compilers
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Software verification

Recommendations

Lutsig: a verified Verilog compiler for verified circuit development
CPP 2021: Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs

We report on a new verified Verilog compiler called Lutsig. Lutsig currently targets (a class of) FPGAs and is capable of producing technology mapped netlists for FPGAs. We have connected Lutsig to existing Verilog development tools, and in this paper ...
Pervasive Compiler Verification -- From Verified Programs to Verified Systems

We report in this paper on the formal verification of a simple compiler for the C-like programming language C0. The compiler correctness proof meets the special requirements of pervasive system verification and allows to transfer correctness properties ...
Verifying verified code
Abstract
A recent case study from AWS by Chong et al. proposes an effective methodology for Bounded Model Checking in industry. In this paper, we report on a follow-up case study that explores the methodology from the perspective of three research ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation

June 2019

1162 pages

ISBN:9781450367127

DOI:10.1145/3314221

General Chair:
Kathryn S. McKinley
Google, USA
,
Program Chair:
Kathleen Fisher
Tufts University, USA

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: 08 June 2019

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Artifacts Evaluated & Functional

Author Tags

Qualifiers

Research-article

Conference

PLDI '19

Sponsor:

SIGPLAN

PLDI '19: 40th ACM SIGPLAN Conference on Programming Language Design and Implementation

June 22 - 26, 2019

AZ, Phoenix, USA

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

14
Total Citations
View Citations
387
Total Downloads

Downloads (Last 12 months)62
Downloads (Last 6 weeks)1

Reflects downloads up to 12 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Athalye ACorrigan-Gibbs HKaashoek FTassarotti JZeldovich NWitchel EArpaci-Dusseau ARossbach CKeeton K(2024)Modular Verification of Secure and Leakage-Free Systems: From Application Specification to Circuit-Level ImplementationProceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles10.1145/3694715.3695956(655-672)Online publication date: 4-Nov-2024
https://dl.acm.org/doi/10.1145/3694715.3695956
Erbsen APhilipoom JJamner DLin AGruetter SPit-Claudel CChlipala A(2024)Foundational Integration Verification of a Cryptographic ServerProceedings of the ACM on Programming Languages10.1145/36564468:PLDI(1704-1729)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656446
Gruetter SFukala VChlipala A(2024)Live Verification in an Interactive Proof AssistantProceedings of the ACM on Programming Languages10.1145/36564398:PLDI(1535-1558)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656439
Athalye AKaashoek FZeldovich NTassarotti J(2023)The K2 Architecture for Trustworthy Hardware Security ModulesProceedings of the 1st Workshop on Kernel Isolation, Safety and Verification10.1145/3625275.3625402(26-32)Online publication date: 23-Oct-2023
https://dl.acm.org/doi/10.1145/3625275.3625402
Barrière ABlazy SPichardie D(2023)Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT CompilerProceedings of the ACM on Programming Languages10.1145/35712027:POPL(249-277)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571202
Tan YHeule MMyreen M(2023)Verified Propagation Redundancy and Compositional UNSAT Checking in CakeMLInternational Journal on Software Tools for Technology Transfer10.1007/s10009-022-00690-y25:2(167-184)Online publication date: 27-Feb-2023
https://doi.org/10.1007/s10009-022-00690-y
Sozeau M(2021)Touring the MetaCoq Project (Invited Paper)Electronic Proceedings in Theoretical Computer Science10.4204/EPTCS.337.2337(13-29)Online publication date: 16-Jul-2021
https://doi.org/10.4204/EPTCS.337.2
Herklotz YPollard JRamanathan NWickerson J(2021)Formal verification of high-level synthesisProceedings of the ACM on Programming Languages10.1145/34854945:OOPSLA(1-30)Online publication date: 15-Oct-2021
https://dl.acm.org/doi/10.1145/3485494
Zhang QWang JKim MSpinellis DGousios GChechik MDi Penta M(2021)HeteroFuzz: fuzz testing to detect platform dependent divergence for heterogeneous applicationsProceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3468264.3468610(242-254)Online publication date: 20-Aug-2021
https://dl.acm.org/doi/10.1145/3468264.3468610
Vega LMcMahan JSampson AGrossman DCeze LFreund SYahav E(2021)Reticle: a virtual machine for programming modern FPGAsProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454075(756-771)Online publication date: 19-Jun-2021
https://dl.acm.org/doi/10.1145/3453483.3454075
Show More Cited By

View Options

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

Lutsig: a verified Verilog compiler for verified circuit development

Pervasive Compiler Verification -- From Verified Programs to Verified Systems

Verifying verified code