Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
Sun 18 Aug 2019 10:50 - 11:30 at Yew - Session 2

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 Aug

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:50 - 12:10
Session 2Erlang at Yew
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