We present our framework for the verification of parameterized infinite-state systems. The framework has been successfully applied in the verification of heterogeneous systems, ranging from distributed fault-tolerant protocols to programs handling unbounded data-structures. In such application doma ins, being able to infer quantified invariants is a mandatory requirement for successful results. Our framework differentiates itself from the state-of-the-art solutions targeting the generation of quantified safe inductive invariants: instead of monolitically exploiting a single static analysis technique, it is based on the effective integration of several analysis strategies. The paper targets the description of the engineering strategies adopted for a successful implementation of such an integrated framework, and presents the extensive experimental evaluation demonstrating its effectiveness.

The elicitation and the analysis of security and privacy requirements are generally intended as being mainly performed by field experts. In this paper we show how it is possible to integrate practical Co-Creation processes into Security-and-Privacy-by-Design methodologies. In addition, we present some guidelines showing how it is possible to translate the high-level requirements obtained from the end-user engaging into verifiable low-level requirements and technological requirements. The paper demonstrates as well the feasibility of our approach by applying it in two realistic scenarios where the outsourcing of personal and sensitive data requires high-level of security and privacy.

Program verification systems fail in verifying programs if appropriate loop invariants are not suggested. Generation of loop invariants in general is an art and providing them manually is a highly complex task (if possible at all). In this paper we present VERIGE, a tool that integrates a verifier with an invariant generator engine. VERIGE implements a novel generic algorithm that can alleviate the load on the invariant generator and consequently achieve a general speed-up of program verification.

Automated techniques for the security analysis of Role-Based Access Control (RBAC) access control policies are crucial for their design and maintenance. The definition of administrative domains by means of attributes attached to users makes the RBAC model easier to use in real scenarios but complicates the development of security analysis techniques, that should be able to modularly reason about a wide range of attribute domains. In this paper, we describe an automated symbolic security analysis technique for administrative attribute-based RBAC policies. A class of formulae of first-order logic is used as an adequate symbolic representation for the policies and their administrative actions. State-of-the-art automated theorem proving techniques are used (off-the-shelf) to mechanize the security analysis procedure. Besides discussing the assumptions for the effectiveness and termination of the procedure, we demonstrate its efficiency through an extensive empirical evaluation.