Formal Verification of an Implementation of the Roughtime Server
Formal verification has been used in the past few decades to prove correctness of programs. This thesis provides a verification of a simpler implementation of Roughtime [1], a protocol that consists of securely querying the current time via a client-server interaction. The tool that was used is Bedr...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Published: |
Massachusetts Institute of Technology
2022
|
| Online Access: | https://hdl.handle.net/1721.1/139971 |
| Summary: | Formal verification has been used in the past few decades to prove correctness of programs. This thesis provides a verification of a simpler implementation of Roughtime [1], a protocol that consists of securely querying the current time via a client-server interaction. The tool that was used is Bedrock2 [3], a work-in-progress Coq framework suitable for reasoning about low-level code, developed in the Programming Languages and Verification group at MIT CSAIL. |
|---|