Code-level model checking in the software development workflow at Amazon Web Services

被引：12

作者：

Chong, Nathan ^{[1
]}

Cook, Byron ^{[1
,2
]}

Eidelman, Jonathan ^{[1
]}

Kallas, Konstantinos ^{[3
]}

Khazem, Kareem ^{[1
]}

Monteiro, Felipe R. ^{[1
]}

Schwartz-Narbonne, Daniel ^{[1
]}

Tasiran, Serdar ^{[1
]}

Tautschnig, Michael ^{[1
,4
]}

Tuttle, Mark R. ^{[1
]}

机构：

[1] Amazon, New York, NY 10001 USA

[2] UCL, London, England

[3] Univ Penn, Philadelphia, PA 19104 USA

[4] Queen Mary Univ London, London, England

来源：

SOFTWARE-PRACTICE & EXPERIENCE | 2021年 / 51卷 / 04期

基金：

英国工程与自然科学研究理事会;

关键词：

continuous integration; model checking; memory safety; FORMAL VERIFICATION; STATIC ANALYSIS;

D O I：

10.1002/spe.2949

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

This article describes a style of applying symbolic model checking developed over the course of four years at Amazon Web Services (AWS). Lessons learned are drawn from proving properties of numerous C-based systems, for example, custom hypervisors, encryption code, boot loaders, and an IoT operating system. Using our methodology, we find that we can prove the correctness of industrial low-level C-based systems with reasonable effort and predictability. Furthermore, AWS developers are increasingly writing their own formal specifications. As part of this effort, we have developed a CI system that allows integration of the proofs into standard development workflows and extended the proof tools to provide better feedback to users. All proofs discussed in this article are publicly available on GitHub.

引用

页码：772 / 797

页数：26

共 48 条

[1]

Aagaard MD., 2000, INT C FORM METH COMP, P300

[2]

Anand, 2018, DANIEL SCHWARTZ NARB

[3] SideTrail: Verifying Time-Balancing of Cryptosystems [J].

Athanasiou, Konstantinos ;

Cook, Byron ;

Emmi, Michael ;

MacCarthaigh, Colm ;

Schwartz-Narbonne, Daniel ;

Tasiran, Serdar .

VERIFIED SOFTWARE: THEORIES, TOOLS, AND EXPERIMENTS, (VSTTE 2018), 2018, 11294 :215-228

[4]

Backes J, 2018, PROCEEDINGS OF THE 2018 18TH CONFERENCE ON FORMAL METHODS IN COMPUTER AIDED DESIGN (FMCAD), P206

[5] Reachability Analysis for AWS-Based Networks [J].

Backes, John ;

Bayless, Sam ;

Cook, Byron ;

Dodge, Catherine ;

Gacek, Andrew ;

Hu, Alan J. ;

Kahsai, Temesghen ;

Kocik, Bill ;

Kotelnikov, Evgenii ;

Kukovec, Jure ;

McLaughlin, Sean ;

Reed, Jason ;

Rungta, Neha ;

Sizemore, John ;

Stalzer, Mark ;

Srinivasan, Preethi ;

Subotic, Pavle ;

Varming, Carsten ;

Whaley, Blake .

COMPUTER AIDED VERIFICATION, CAV 2019, PT II, 2019, 11562 :231-241

[6]

Ball T, 2004, LECT NOTES COMPUT SC, V2999, P1

[7] A Few Billion Lines of Code Later Using Static Analysis to Find Bugs in the Real World [J].

Bessey, Al ;

Block, Ken ;

Chelf, Ben ;

Chou, Andy ;

Fulton, Bryan ;

Hallem, Seth ;

Henri-Gros, Charles ;

Kamsky, Asya ;

McPeak, Scott ;

Engler, Dawson .

COMMUNICATIONS OF THE ACM, 2010, 53 (02) :66-75

[8] Automatic Verification of C and Java']Java Programs: SV-COMP 2019 [J].

Beyer, Dirk .

TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT III, 2019, 11429 :133-155

[9] Moving Fast with Software Verification [J].

Calcagno, Cristiano ;

Distefano, Dino ;

Dubreil, Jeremy ;

Gabi, Dominik ;

Hooimeijer, Pieter ;

Luca, Martino ;

O'Hearn, Peter ;

Papakonstantinou, Irene ;

Purbrick, Jim ;

Rodriguez, Dulma .

NASA FORMAL METHODS (NFM 2015), 2015, 9058 :3-11

[10]

Calcagno C, 2011, LECT NOTES COMPUT SC, V6617, P459, DOI 10.1007/978-3-642-20398-5_33

← 1 2 3 4 5 →