-
CTL* Verification and Synthesis using Existential Horn Clauses
Authors:
Mishel Carelli,
Orna Grumberg
Abstract:
This work proposes a novel approach for automatic verification and synthesis of infinite-state reactive programs with respect to ${CTL}^*$ specifications, based on translation to Existential Horn Clauses (EHCs).
$CTL^*$ is a powerful temporal logic, which subsumes the temporal logics LTL and CTL, both widely used in specification, verification, and synthesis of complex systems.
EHCs with its s…
▽ More
This work proposes a novel approach for automatic verification and synthesis of infinite-state reactive programs with respect to ${CTL}^*$ specifications, based on translation to Existential Horn Clauses (EHCs).
$CTL^*$ is a powerful temporal logic, which subsumes the temporal logics LTL and CTL, both widely used in specification, verification, and synthesis of complex systems.
EHCs with its solver E-HSF, is an extension of Constrained Horn Clauses, which includes existential quantification as well as the power of handling well-foundedness.
We develop the translation system \textit{Trans}, which given a verification problem consisting of a program $P$ and a specification $φ$, builds a set of EHCs which is satisfiable iff $P$ satisfies $φ$. We also develop a synthesis algorithm that given a program with holes in conditions and assignments, fills the holes so that the synthesized program satisfies the given $CTL^*$ specification.
We prove that our verification and synthesis algorithms are both sound and relative complete. Finally, we present case studies to demonstrate the applicability of our algorithms for $CTL^*$ verification and synthesis.
△ Less
Submitted 21 August, 2024;
originally announced August 2024.
-
Assume, Guarantee or Repair -- A Regular Framework for Non Regular Properties (full version)
Authors:
Hadar Frenkel,
Orna Grumberg,
Corina S. Pasareanu,
Sarai Sheinvald
Abstract:
We present Assume-Guarantee-Repair (AGR) - a novel framework which verifies that a program satisfies a set of properties and also repairs the program in case the verification fails. We consider communicating programs - these are simple C-like programs, extended with synchronous actions over communication channels. Our method, which consists of a learning-based approach to assume-guarantee reasonin…
▽ More
We present Assume-Guarantee-Repair (AGR) - a novel framework which verifies that a program satisfies a set of properties and also repairs the program in case the verification fails. We consider communicating programs - these are simple C-like programs, extended with synchronous actions over communication channels. Our method, which consists of a learning-based approach to assume-guarantee reasoning, performs verification and repair simultaneously: in every iteration, AGR either makes another step towards proving that the (current) system satisfies the required properties, or alters the system in a way that brings it closer to satisfying the properties. To handle infinite-state systems we build finite abstractions, for which we check the satisfaction of complex properties that contain first-order constraints, using both syntactic and semantic-aware methods. We implemented AGR and evaluated it on various communication protocols. Our experiments present compact proofs of correctness and quick repairs.
△ Less
Submitted 21 July, 2022;
originally announced July 2022.
-
Modular Verification of Concurrent Programs via Sequential Model Checking
Authors:
Dan Rasin,
Orna Grumberg,
Sharon Shoham
Abstract:
This work utilizes the plethora of work on verification of sequential programs for the purpose of verifying concurrent programs. We reduce the verification of a concurrent program to a series of verification tasks of sequential programs. Our approach is modular in the sense that each sequential verification task roughly corresponds to the verification of a single thread, with some additional infor…
▽ More
This work utilizes the plethora of work on verification of sequential programs for the purpose of verifying concurrent programs. We reduce the verification of a concurrent program to a series of verification tasks of sequential programs. Our approach is modular in the sense that each sequential verification task roughly corresponds to the verification of a single thread, with some additional information about the environment in which it operates. Information regarding the environment is gathered during the run of the algorithm, by need.
While our approach is general, it specializes on concurrent programs where the threads are structured hierarchically. The idea is to exploit the hierarchy in order to minimize the amount of information that needs to be transferred between threads. To that end, we verify one of the threads, considered "main", as a sequential program. Its verification process initiates queries to its "environment" (which may contain multiple threads). Those queries are answered by sequential verification, if the environment consists of a single thread, or, otherwise, by applying the same hierarchical algorithm on the environment.
Our technique is fully automatic, and allows us to use any off-the-shelf sequential model checker. We implemented our technique in a tool called CoMuS and evaluated it against established tools for concurrent verification. Our experiments show that it works particularly well on hierarchically structured programs.
△ Less
Submitted 1 June, 2021;
originally announced June 2021.
-
Formal Black-Box Analysis of Routing Protocol Implementations
Authors:
Adi Sosnovich,
Orna Grumberg,
Gabi Nakibly
Abstract:
The Internet infrastructure relies entirely on open standards for its routing protocols. However, the majority of routers on the Internet are closed-source. Hence, there is no straightforward way to analyze them. Specifically, one cannot easily identify deviations of a router's routing functionality from the routing protocol's standard. Such deviations (either deliberate or inadvertent) are partic…
▽ More
The Internet infrastructure relies entirely on open standards for its routing protocols. However, the majority of routers on the Internet are closed-source. Hence, there is no straightforward way to analyze them. Specifically, one cannot easily identify deviations of a router's routing functionality from the routing protocol's standard. Such deviations (either deliberate or inadvertent) are particularly important to identify since they may degrade the security or resiliency of the network.
A model-based testing procedure is a technique that allows to systematically generate tests based on a model of the system to be tested; thereby finding deviations in the system compared to the model. However, applying such an approach to a complex multi-party routing protocol requires a prohibitively high number of tests to cover the desired functionality. We propose efficient and practical optimizations to the model-based testing procedure that are tailored to the analysis of routing protocols. These optimizations allow to devise a formal black-box method to unearth deviations in closed-source routing protocols' implementations. The method relies only on the ability to test the targeted protocol implementation and observe its output. Identification of the deviations is fully automatic.
We evaluate our method against one of the complex and widely used routing protocols on the Internet -- OSPF. We search for deviations in the OSPF implementation of Cisco. Our evaluation identified numerous significant deviations that can be abused to compromise the security of a network. The deviations were confirmed by Cisco. We further employed our method to analyze the OSPF implementation of the Quagga Routing Suite. The analysis revealed one significant deviation. Subsequent to the disclosure of the deviations some of them were also identified by IBM, Lenovo and Huawei in their own products.
△ Less
Submitted 23 September, 2017;
originally announced September 2017.
-
Learning to Order BDD Variables in Verification
Authors:
O. Grumberg,
S. Livne,
S. Markovitch
Abstract:
The size and complexity of software and hardware systems have significantly increased in the past years. As a result, it is harder to guarantee their correct behavior. One of the most successful methods for automated verification of finite-state systems is model checking. Most of the current model-checking systems use binary decision diagrams (BDDs) for the representation of the te…
▽ More
The size and complexity of software and hardware systems have significantly increased in the past years. As a result, it is harder to guarantee their correct behavior. One of the most successful methods for automated verification of finite-state systems is model checking. Most of the current model-checking systems use binary decision diagrams (BDDs) for the representation of the tested model and in the verification process of its properties. Generally, BDDs allow a canonical compact representation of a boolean function (given an order of its variables). The more compact the BDD is, the better performance one gets from the verifier. However, finding an optimal order for a BDD is an NP-complete problem. Therefore, several heuristic methods based on expert knowledge have been developed for variable ordering. We propose an alternative approach in which the variable ordering algorithm gains 'ordering experience' from training models and uses the learned knowledge for finding good orders. Our methodology is based on offline learning of pair precedence classifiers from training models, that is, learning which variable pair permutation is more likely to lead to a good order. For each training model, a number of training sequences are evaluated. Every training model variable pair permutation is then tagged based on its performance on the evaluated orders. The tagged permutations are then passed through a feature extractor and are given as examples to a classifier creation algorithm. Given a model for which an order is requested, the ordering algorithm consults each precedence classifier and constructs a pair precedence table which is used to create the order. Our algorithm was integrated with SMV, which is one of the most widely used verification systems. Preliminary empirical evaluation of our methodology, using real benchmark models, shows performance that is better than random ordering and is competitive with existing algorithms that use expert knowledge. We believe that in sub-domains of models (alu, caches, etc.) our system will prove even more valuable. This is because it features the ability to learn sub-domain knowledge, something that no other ordering algorithm does.
△ Less
Submitted 30 June, 2011;
originally announced July 2011.
