Logo: to the web site of Uppsala University

Existing active automata learning (AAL) algorithms have demonstrated their potential in capturing the behavior of complex systems (e.g., in analyzing network protocol implementations). The most widely used AAL algorithms generate finite state machine models, such as Mealy machines or deterministic finite automata. For many analysis tasks, however, it is crucial to generate richer classes of models that also show how relations between data parameters affect system behavior. Such models have shown potential to uncover critical bugs, but their learning algorithms do not scale beyond small and well curated experiments. In this article, we present SL^λ, an effective and scalable register automata (RA) learning algorithm that significantly reduces the number of membership queries required for inferring models. It achieves this by combining a tree-based cost-efficient data structure with mechanisms for computing short and restricted tests. We prove that SL^λ is guaranteed to learn an acceptor, in the form of a register automaton with n locations and t transitions, for a given data language of finite index, and that it can do so with at most O(t²(2n)ⁿ+mt²m^m) membership queries and O(t) equivalence queries, where m is the length of the longest counterexample received during learning. We have implemented SL^λ as a new algorithm in RALib. We evaluate its performance by comparing it against SL^∗, the current state-of-the-art RA learning algorithm. Experiments on a series of benchmarks show that it reduces the number of membership queries by up to an order of magnitude, and also shows substantial asymptotic improvements in bigger systems. 

Stateless Model Checking (SMC) is a verification technique for concurrent programs that checks for safety violations by exploring all possible thread schedulings. It is highly effective when coupled with Dynamic Partial Order Reduction (DPOR), which introduces an equivalence on schedulings and allows SMC to explore only one execution per equivalence class. Even with DPOR, SMC often spends unnecessary effort in exploring loop iterations that are pure, i.e., have no effect on the program state. In this article, we present techniques for making SMC with DPOR more effective on programs with pure loop iterations. The first technique is a static program analysis to detect loop purity and an associated program transformation, called Partial Loop Purity Elimination, that inserts assume statements to block pure loop iterations. Subsequently, some of these assume statements are turned into await statements that completely remove many assume-blocked executions. Finally, we present an extension of the standard DPOR equivalence, obtained by weakening the conflict relation between events. All these techniques are incorporated into a new DPOR algorithm, Optimal-DPOR-Await, which can handle both await statements and the weaker conflict relation, is optimal in the sense that it explores exactly one execution in each equivalence class, and can also diagnose livelocks. Our implementation in Nidhugg shows that these techniques can significantly speed up the analysis of concurrent programs that are currently challenging for SMC tools, both for exploring their complete set of interleavings, but even for detecting concurrency errors in them.

This paper revisits the fundamental problem of monitoring the linearizability of concurrent stacks, queues, sets, and multisets.

Given a history of a library implementing one of these abstract data types, the monitoring problem is to answer whether the given history is linearizable.

For stacks, queues, and (multi)sets, we present monitoring algorithms with complexities (n²), (n log n), and (n), respectively, where n is the number of operations in the input history.

For stacks and queues, our results hold under the standard assumption of data-independence, i.e., the behavior of the library is not sensitive to the actual values stored in the data structure.

Past works to solve the same problems have cubic time complexity and (more seriously) have correctness issues: they either (i) lack correctness proofs or (ii) have unsound correctness proofs (we present counter-examples of the correctness proofs), or (iii) have unsound algorithms.

Our improved complexity results rely on substantially different algorithms for which we provide detailed proofs of correctness.

We have implemented our stack and queue algorithms in LiMo (Linearizability Monitor). We evaluate LiMo and compare it with the state-of-the-art tool Violin – whose correctness proofs we have found errors in – which checks for linearizability violations. Our experimental evaluation confirms that LiMo outperforms Violin regarding both efficiency and scalability.

Deterministic models play a crucial role in computer system development, enabling the simulation and verification of system behaviors before ModelDriven Development (MDD) tools transform and compile these models into final implementations. Ensuring determinism is essential to guarantee that the behaviors of the implemented system maintain the properties analyzed in the models.

This paper investigates the semantics of deterministic models for data-flow networks, where systems consist of components that compute functions on streams. While Kahn Process Networks (KPN) serve as a well-established semantic theory for time-insensitive deterministic systems, it proves inadequate for systems with time dependent components. To address this limitation, we use the concept of timed streams and develop a fixed-point theory tailored for time-sensitive systems in the style of KPN. This theory serves as the foundation for the MDD tool-chain, known as MIMOS, currently under development in Uppsala.

Implementations of network protocols must conform to their specifications in order to avoid security vulnerabilities and interoperability issues. To detect errors, testing must investigate an implementation's response to a wide range of inputs, including those that could be supplied by an attacker. This can be achieved by symbolic execution, but its application in testing network protocol implementations has so far been limited. One difficulty when testing such implementations is that the inputs and requirements for processing a packet depend on the sequence of previous packets. We present a novel technique to encode protocol requirements by monitors, and then employ symbolic execution to detect violations of these requirements in protocol implementations. A monitor is a component external to the SUT, that observes a sequence of packets exchanged between protocol parties, maintains information about the state of the interaction, and can thereby detect requirement violations. Using monitors, requirements for stateful network protocols can be tested with a wide variety of inputs, without intrusive modifications in the source code of the SUT. We have applied our technique on the most recent versions of several widely-used DTLS and QUIC protocol implementations, and have been able to detect twenty two previously unknown bugs in them, twenty one of which have already been fixed and the remaining one has been confirmed.

Statelessmodel checking is a fully automatic verification technique for concurrent programs that checks for safety violations by exploring all possible thread schedulings. It becomes effective when coupled with Dynamic Partial Order Reduction (DPOR), which introduces an equivalence on schedulings and reduces the amount of needed exploration. DPOR algorithms that are optimal are particularly effective in that they guarantee to explore exactly one execution from each equivalence class. Unfortunately, existing sequence-based optimal algorithms may in the worst case consume memory that is exponential in the size of the analyzed program. In this paper, we present Parsimonious-OPtimal DPOR (POP), an optimal DPOR algorithm for analyzing multi-threaded programs under sequential consistency, whose space consumption is polynomial in the worst case. POP combines several novel algorithmic techniques, including (i) a parsimonious race reversal strategy, which avoids multiple reversals of the same race, (ii) an eager race reversal strategy to avoid storing initial fragments of to-be-explored executions, and (iii) a space-efficient scheme for preventing redundant exploration, which replaces the use of sleep sets. Our implementation in Nidhugg shows that these techniques can significantly speed up the analysis of concurrent programs, and do so with low memory consumption. Comparison to TruSt, a related optimal DPOR algorithm that represents executions as graphs, shows that POP's implementation achieves similar performance for smaller benchmarks, and scales much better than TruSt's on programs with long executions.

Existing active automata learning (AAL) algorithms have demonstrated their potential in capturing the behavior of complex systems (e.g., in analyzing network protocol implementations). The most widely used AAL algorithms generate finite state machine models, such as Mealy machines. For many analysis tasks, however, it is crucial to generate richer classes of models that also show how relations between data parameters affect system behavior. Such models have shown potential to uncover critical bugs, but their learning algorithms do not scale beyond small and well curated experiments. In this paper, we present SL^λ, an effective and scalable register automata (RA) learning algorithm that significantly reduces the number of tests required for inferring models. It achieves this by combining a tree-based cost-efficient data structure with mechanisms for computing short and restricted tests. We have implemented SL^λ as a new algorithm in RALib. We evaluate its performance by comparing it against SL*, the current state-of-the-art RA learning algorithm, in a series of experiments, and show superior performance and substantial asymptotic improvements in bigger systems.

Implementations of stateful network protocols must keep track of the presence, order and type of exchanged messages. Any errors, socalled 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.

The rapid expansion of the Internet of Things (IoT) has introduced the need for thorough testing of its protocol implementations to ensure conformance to their specifications and increase their security. This paper investigates the application of two of the major testing techniques, fuzz testing and symbolic execution, to test the implementations of the Constrained Application Protocol (CoAP), a key protocol in the IoT ecosystem. We explore the efficacy of these techniques in discovering requirement violations in CoAP implementations. Focusing on two widely-used CoAP implementations, libcoap and FreeCoAP, we systematically apply both fuzzing and symbolic execution to test conformance with key requirements derived from CoAP's specifications. Our findings demonstrate the strengths and limitations of both approaches, and highlight nine nonconformances in these implementations, most of which have been fixed. Finally, we provide insights into how fuzzing and symbolic execution can be effectively utilized for protocol testing.

Stateless model checking is a fully automatic verification technique for concurrent programs, which checks for safety violations by exploring all possible thread schedulings. It becomes effective when coupled with Dynamic Partial Order Reduction (DPOR), which introduces an equivalence on schedulings and reduces the amount of exploration. DPOR algorithms that are optimal are particularly effective in that they guarantee to explore exactly one execution from each equivalence class. Recently, the authors of this paper presented Parsimonious-OPtimal (POP) DPOR, an optimal DPOR algorithm for analyzing multi-threaded programs under sequential consistency, whose space consumption is polynomial in the worst case. This space consumption bound was realized due to a carefully crafted encoding of so-called sleep sets, a mechanism for preventing redundant exploration. This encoding brings some conceptual complexity to POP, which achieves good worst-case performance at the possible expense of worse average-case performance. In this paper, we present a simpler technique for managing sleep sets, which has exponential worst-case space consumption but better average-case performance. We experimentally compare these two sleep set management schemes on a range of benchmarks. The experimental results confirm that a simpler sleep set is a better choice when designing DPOR algorithms as they are faster and have similar memory consumption for average programs.