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 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.

Name thesis:degree_name

Master

Department dc:contributor.department

Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science

Grantor dc:publisher

Massachusetts Institute of Technology

Year dc:date.issued

2021

Author dc:creator

• Altamirano, Christian

Advisor dc:contributor.advisor

• Chlipala, Adam

Statement dc:rights

• In Copyright - Educational Use Permitted
• Copyright MIT

Licence dc:rights.uri

• http://rightsstatements.org/page/InC-EDU/1.0/

Handle dc:identifier.uri

https://hdl.handle.net/1721.1/139971

OAI identifier oai:identifier

oai:dspace.mit.edu:1721.1/139971