RecordFlux:形式化消息规范与可验证二进制解析器的生成
编程语言
2019-10-08 v1 密码学与安全
网络与互联网体系结构
摘要
过去在协议实现的消息解析器中发现了各种漏洞。即便是高度敏感的软件组件如 TLS 库也经常受影响。由此引发的问题从拒绝服务攻击到敏感信息提取不等。协议的复杂性与自然语言规范的不精确是实现中难以发现的细微错误的核心原因。缺乏精确规范阻碍了形式化验证。在本文中,我们提出一个模型及相应的领域特定语言,用以形式化规范现有真实世界二进制协议的消息格式。该模型的一个独特功能是能够定义不变量,即规定消息字段间的关系与依赖。此外,该模型允许定义不同协议层间消息的关系,从而确保对载荷数据的正确解释。我们提出一种基于该模型推导可验证解析器、生成高效实现代码并自动证明无运行时错误的技术。针对 Ethernet 与 TLS 的解析器规范示例展示了我们方法的适用性。
引用
@article{arxiv.1910.02146,
title = {RecordFlux: Formal Message Specification and Generation of Verifiable Binary Parsers},
author = {Tobias Reiher and Alexander Senier and Jeronimo Castrillon and Thorsten Strufe},
journal= {arXiv preprint arXiv:1910.02146},
year = {2019}
}