Gaining Trust by Tracing Security Protocols
In this article we test an Erlang implementation of the Noise Protocol Framework, using a novel form of white-box testing. We extend interoperability testing of an Erlang enoise imple- mentation against an implementation of Noise in C. Testing typically performs a noise protocol handshake between the two implementations. If successful, then both implementa- tions are somehow compatible. But this does, for example, not detect whether we reuse keys that have to be newly gen- erated. Therefore we extend such operability testing: During the handshake the Erlang noise implementation is traced. The resulting protocol trace is refactored, obtaining as the end result a symbolic description (a functional term) of how key protocol values are constructed using cryptographic op- erations and keys. Therafter, this symbolic term is compared, using term rewriting, with a symbolic term representing the ideal symbolic execution of the tested noise protocol hand- shake (i.e., the “semantics” of the handshake). The semantic symbolic term is obtained by executing a symbolic imple- mentation of the noise protocol that we have developed.
Sun 18 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:50 - 12:10
|Gaining Trust by Tracing Security Protocols|
Lars-Ake Fredlund , Thomas Arts Quviq, Clara Benac Earle Universidad Politécnica de Madrid, Hans Svensson Quviq AB
|Runtime Type Safety for Erlang/OTP Behaviours|
Joseph Harrison University of Kent, UK