Broadcast protocols (BPs) are a formal model of distributed systems with an unbounded number of processes communicating through broadcasts. We study the problem of passively learning BPs from execution traces, focusing on the class of fine BPs which does not have hidden states and admits a cutoff. We present a passive learning algorithm with a constraint-based approach that guarantees consistency with the sample, and returns a minimal equivalent BP if the sample is sufficiently complete (i.e., subsumes a characteristic set). Furthermore, we describe LeoParDS, the first tool that implements these techniques, supporting the practical inference of fine BPs, as well as tasks that include sample generation and approximate equivalence checking. This work was previously published at AAAI’24 [8] and later implemented at ATVA’24 [12]. We summarize its main results here to foster discussion within the cybersecurity and verification community. This short paper is intended as a concise overview for readers unfamiliar with both prior publications.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Insights into Learning Broadcast Protocols

  • Dana Fisman,
  • Noa Izsak,
  • Swen Jacobs

摘要

Broadcast protocols (BPs) are a formal model of distributed systems with an unbounded number of processes communicating through broadcasts. We study the problem of passively learning BPs from execution traces, focusing on the class of fine BPs which does not have hidden states and admits a cutoff. We present a passive learning algorithm with a constraint-based approach that guarantees consistency with the sample, and returns a minimal equivalent BP if the sample is sufficiently complete (i.e., subsumes a characteristic set). Furthermore, we describe LeoParDS, the first tool that implements these techniques, supporting the practical inference of fine BPs, as well as tasks that include sample generation and approximate equivalence checking. This work was previously published at AAAI’24 [8] and later implemented at ATVA’24 [12]. We summarize its main results here to foster discussion within the cybersecurity and verification community. This short paper is intended as a concise overview for readers unfamiliar with both prior publications.