Abstract by Matthew Christensen

Personal Infomation

Presenter's Name

Matthew Christensen


Cheyenne Son Davis

Degree Level



Cheyenne Son Davis

Abstract Infomation


Computer Science

Faculty Advisor

Eric Mercer
Daniel Zappala


Formal Methods of Verification


The computer science industry currently relies on informal methods of verification to ensure the security of software, which fail to detect many underlying errors in software leading to vulnerable software. Errors are especially prevalent in applications that use TLS for encryption. The TLS protocol is very complex, which leads developers to unknowingly use TLS incorrectly. We present our efforts to formally verify the Secure Socket API (SSA), an attempt to simplify the correct use of TLS. We create sequence diagrams to understand the call graph of the API. Next, we specify contracts to define a weakest precondition calculus based off of a list of secure socket properties. We use Dafny to verify that the contracts ensure the security properties over the state space in the SSA, thus guarenting secure TLS connections.