Security protocols are essential building blocks of modern IT systems. Subtle flaws in their design or implementation may compromise the security of entire systems. It is, thus, important to prove the absence of such flaws through formal verification. Much existing work focuses on the verification of protocol *models*, which is not sufficient to show that their *implementations* are actually secure. Verification techniques for protocol implementations (e.g., via code generation or model extraction) typically impose severe restrictions on the used programming language and code design, which may lead to sub-optimal implementations. In this paper, we present a methodology for the modular verification of strong security properties directly on the level of the protocol implementations. Our methodology leverages state-of-the-art verification logics and tools to support a wide range of implementations and programming languages. We demonstrate its effectiveness by verifying memory safety and security of Go implementations of the Needham-Schroeder-Lowe and WireGuard protocols, including forward secrecy and injective agreement for WireGuard. We also show that our methodology is agnostic to a particular language or program verifier with a prototype implementation for C.
翻译:安全协议是现代信息技术系统的基本构件。其设计或执行中的细微缺陷可能会损害整个系统的安全。因此,通过正式核查证明不存在这种缺陷非常重要。许多现有工作侧重于核查协议* 模型* 的核查,这不足以表明其* 执行* 实际是安全的。协议执行的核查技术(例如,通过代码生成或模式提取)通常对所使用的编程语言和代码设计施加严格的限制,可能导致次优执行。在本文件中,我们提出了直接在协议执行水平上对强力安全特性进行模块化核查的方法。我们的方法利用了最先进的核查逻辑和工具来支持广泛的实施和编程语言。我们通过核查执行协议(例如,通过代码生成或模式提取)的记忆安全和安保,包括远端保密和WireGuard的预言协议,证明了其有效性。我们还表明,我们的方法对于特定语言或程序与执行原型C的核查程序具有不确定性。