Name
Abstract | ||
|---|---|---|
Recent advances in formal verification techniques enabled the implementation of distributed systems with machine-checked proofs. While results are encouraging, the importance of distributed systems warrants a large scale evaluation of the results and verification practices. This paper thoroughly analyzes three state-of-the-art, formally verified implementations of distributed systems: Iron-Fleet, Verdi, and Chapar. Through code review and testing, we found a total of 16 bugs, many of which produce serious consequences, including crashing servers, returning incorrect results to clients, and invalidating verification guarantees. These bugs were caused by violations of a wide-range of assumptions on which the verified components relied. Our results revealed that these assumptions referred to a small fraction of the trusted computing base, mostly at the interface of verified and unverified components. Based on our observations, we have built a testing toolkit called PK, which focuses on testing these parts and is able to automate the detection of 13 (out of 16) bugs. |
Year | DOI | Venue |
|---|---|---|
2017 | 10.1145/3064176.3064183 | EuroSys |
Field | DocType | Citations |
Programming language,Computer science,Concurrency,Server,Correctness,Real-time computing,Mathematical proof,Trusted computing base,Mutual exclusion,Code review,Formal verification,Distributed computing | Conference | 12 |
PageRank | References | Authors |
0.60 | 37 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Pedro Fonseca | 1 | 83 | 4.23 |
| Kaiyuan Zhang | 2 | 22 | 3.17 |
| Xi Wang | 3 | 540 | 29.04 |
| Arvind Krishnamurthy | 4 | 4540 | 312.24 |