Active Intruders with Caps - Anatharaman, Siva; Lin, Hai; Lynch, Chris; Narendran, Paliath; Rusinowitch, Michael
Combination of Convex Theories: Modularity, Deduction Completeness, and Explanation - Tran, Duc-Khanh; Ringeissen, Christophe; Ranise, Silvio; Kirchner, Hélène
Decision procedures are key components of theorem provers and constraint satisfaction systems. Their modular combination is of prime interest for building efficient systems, but their effective use is often limited by poor interface capabilities, when such procedures only provide a simple ``sat/unsat'' answer. In this paper, we develop a rule-based framework to design cooperation schemas between such procedures while maintaining modularity of their interfaces. First, we use the rule-based framework to specify and prove the correctness of classic combination schemas by Nelson-Oppen and Shostak. Second, we introduce the concept of deduction complete satisfiability procedures, we show how to build them...
Satisfiability Procedures for Combination of Theories Sharing Integer Offsets - Nicolini, Enrica; Ringeissen, Christophe; Rusinowitch, Michael
We present a novel technique to combine satisfiability procedures for theories that model some data-structures and that share the integer offsets. This procedure extends the Nelson-Oppen approach to a family of non-disjoint theories that have practical interest in verification. The result is derived by showing that the considered theories satisfy the hypotheses of a general result on non-disjoint combination. In particular, the capability of computing logical consequences over the shared signature is ensured in a non trivial way by devising a suitable complete superposition calculus.
Combinable Extensions of Abelian Groups - Nicolini, Enrica; Ringeissen, Christophe; Rusinowitch, Michael
The design of decision procedures for combinations of theories sharing some arithmetic fragment is a challenging problem in verification. One possible solution is to apply a combination method à la Nelson-Oppen, like the one developed by Ghilardi for unions of non-disjoint theories. We show how to apply this non-disjoint combination method with the theory of abelian groups as shared theory. We consider the completeness and the effectiveness of this non-disjoint combination method. For the completeness, we show that the theory of abelian groups can be embedded into a theory admitting quantifier elimination. For achieving effectiveness, we rely on a superposition...
Modular Security Policy Design based on Extended Petri Nets - Huang, Hejiao; Kirchner, Helene
Security policies are one of the most fundamental elements of computer security. Their design has to cope with composition of components in security systems and interactions between them. Consequently, a modular approach for specification and verification of security policies is necessary and the composition of modules must consistently ensure fundamental properties of security policies, in a rigorous and systematic way. This paper shows how to use extended Petri net process (EPNP) to specify and verify security policies in a modular way. It defines a few fundamental policy properties, namely completeness, termination, consistency and confluence, in Petri net terminology and relates...
Secure Interoperation in Heterogeneous Systems based on Colored Petri Nets - Huang, Hejiao; Kirchner, Helene
In a multi-domains application environment, where distributed multiple organizations interoperate with each other, the local access control policies should correspondingly be integrated in order to allow users of one organization to interact with other domains. One of the key challenges of integrating policies is conflict detection and resolution while preserving policy consistency. This paper addresses several types of potential conflicts and consistency properties with a systematic and rigorous approach. In the approach, graph theory, network flow technology and colored Petri nets are applied for specifying and verifying a secure interoperation design. The component-based integration of policies is applicable for both...
Data Structures with Arithmetic Constraints: a Non-Disjoint Combination - Nicolini, Enrica; Ringeissen, Christophe; Rusinowitch, Michael
We apply an extension of the Nelson-Oppen combination method to develop a decision procedure for the non-disjoint union of theories modeling data structures with a counting operator and fragments of arithmetic. We present some data structures and some fragments of arithmetic for which the combination method is complete and effective. To achieve effectiveness, the combination method relies on particular procedures to compute sets that are representative of all the consequences over the shared theory. We show how to compute these sets by using a superposition calculus for the theories of the considered data structures and various solving and reduction techniques...