Gaining trust by tracing security protocols

• Published in: Journal of logical and algebraic methods in programming 2023-01, Vol.130, p.100829, Article 100829
• Main Authors: Fredlund, Lars-Åke, Benac Earle, Clara, Arts, Thomas, Svensson, Hans
• Format: Article
• Language: English
• Subjects: Erlang; Noise Security Protocols; Security protocols; Tracing
• ISSN: 2352-2208
• DOI: 10.1016/j.jlamp.2022.100829

In this article, a novel form of white-box testing is used to test an implementation of the Noise Cryptographic Protocol Framework, which is used as an integral component in a commercial blockchain. Our approach extends the normal interoperability testing, where the noise implementation under test, written in the Erlang programming language, is tested against an implementation of the Noise protocol framework written in the C programming language. Testing typically performs a noise protocol handshake between the two implementations. If successful, then both implementations are considered compatible. However, such testing does not, for example, detect whether the Erlang implementation incorrectly reuse session keys that should have been newly generated. In this article, such interoperability testing is extended to also check that keys and information transmitted in protocol handshakes is correctly constructed, e.g., that session keys are freshly generated by calling the correct low-level cryptographic libraries. Such extended, white-box testing, begins by tracing the Erlang Noise implementation during protocol handshakes with the C programming protocol implementation. 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 operations and keys. Thereafter, this symbolic term is compared, using term rewriting, with another symbolic term representing the ideal symbolic execution of the tested Noise protocol handshake, i.e., the “semantics” of the handshake. The semantic symbolic term is obtained by executing a symbolic implementation of the noise protocol that we have developed, which very closely follows the semi-formal authoritative description of the Noise protocol framework.