BYU

Abstract by Matthew Christensen

Personal Infomation


Presenter's Name

Matthew Christensen

Co-Presenters

Cheyenne Son Davis

Degree Level

Undergraduate

Co-Authors

Cheyenne Son Davis

Abstract Infomation


Department

Computer Science

Faculty Advisor

Eric Mercer
Daniel Zappala

Title

Formal Methods of Verification

Abstract

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.