一句话：提出黑盒测试框架 SMBugFinder，按漏洞模式自动生成并验证暴露协议状态机缺陷的消息序列。
有状态的网络协议实现必须正确跟踪消息的存在、顺序与类型，否则会产生可危及安全的状态机漏洞。SMBugFinder 是一个自动化黑盒测试框架：它接收被测协议实现的状态机模型，以及以有限自动机形式给出的协议漏洞模式目录，自动生成能够暴露这些漏洞的消息序列；通过连接测试桩（harness）对序列进行验证。此前工作已成功评估于 DTLS 与 SSH，本文从用户视角以 EDHOC 协议为例介绍该工具。
Implementations of stateful network protocols must keep track of the presence, order and type of exchanged messages. Any errors, so-called state machine bugs, can compromise security. SMBugFinder provides an automated framework for detecting these bugs in network protocol implementations using black-box testing. It takes as input a state machine model of the protocol implementation which is tested and a catalogue of bug patterns for the protocol conveniently specified as finite automata. It then produces sequences that expose the catalogued bugs in the tested implementation. Connection to a harness allows SMBugFinder to validate these sequences. The technique behind SMBugFinder has been evaluated successfully on DTLS and SSH in prior work. In this paper, we provide a user-level view of the tool using the EDHOC protocol as an example.
@inproceedings{paperbot8551,
title = {SMBugFinder: An Automated Framework for Testing Protocol Implementations for State Machine Bugs},
author = {Paul Fiterău-Broştean and Bengt Jonsson and Konstantinos Sagonas and Fredrik Tåquist},
booktitle = {ISSTA},
year = {2024},
doi = {10.1145/3650212.3685310}
}