-
CAISAR: A platform for Characterizing Artificial Intelligence Safety and Robustness
Authors:
Julien Girard-Satabin,
Michele Alberti,
François Bobot,
Zakaria Chihani,
Augustin Lemesle
Abstract:
We present CAISAR, an open-source platform under active development for the characterization of AI systems' robustness and safety. CAISAR provides a unified entry point for defining verification problems by using WhyML, the mature and expressive language of the Why3 verification platform. Moreover, CAISAR orchestrates and composes state-of-the-art machine learning verification tools which, individ…
▽ More
We present CAISAR, an open-source platform under active development for the characterization of AI systems' robustness and safety. CAISAR provides a unified entry point for defining verification problems by using WhyML, the mature and expressive language of the Why3 verification platform. Moreover, CAISAR orchestrates and composes state-of-the-art machine learning verification tools which, individually, are not able to efficiently handle all problems but, collectively, can cover a growing number of properties. Our aim is to assist, on the one hand, the V\&V process by reducing the burden of choosing the methodology tailored to a given verification problem, and on the other hand the tools developers by factorizing useful features-visualization, report generation, property description-in one platform. CAISAR will soon be available at https://git.frama-c.com/pub/caisar.
△ Less
Submitted 21 June, 2022; v1 submitted 7 June, 2022;
originally announced June 2022.
-
A Deductive Verification Framework for Circuit-building Quantum Programs
Authors:
Christophe Chareton,
Sébastien Bardin,
François Bobot,
Valentin Perrelle,
Benoit Valiron
Abstract:
While recent progress in quantum hardware open the door for significant speedup in certain key areas, quantum algorithms are still hard to implement right, and the validation of such quantum programs is a challenge. Early attempts either suffer from the lack of automation or parametrized reasoning, or target high-level abstract algorithm description languages far from the current de facto consensu…
▽ More
While recent progress in quantum hardware open the door for significant speedup in certain key areas, quantum algorithms are still hard to implement right, and the validation of such quantum programs is a challenge. Early attempts either suffer from the lack of automation or parametrized reasoning, or target high-level abstract algorithm description languages far from the current de facto consensus of circuit-building quantum programming languages. As a consequence, no significant quantum algorithm implementation has been currently verified in a scale-invariant manner. We propose Qbricks, the first formal verification environment for circuit-building quantum programs, featuring clear separation between code and proof, parametric specifications and proofs, high degree of proof automation and allowing to encode quantum programs in a natural way, i.e. close to textbook style. Qbricks builds on best practice of formal verification for the classical case and tailor them to the quantum case: we bring a new domain-specific circuit-building language for quantum programs, namely Qbricks-DSL, together with a new logical specification language Qbricks-Spec and a dedicated Hoare-style deductive verification rule named Hybrid Quantum Hoare Logic. Especially, we introduce and intensively build upon HOPS, a higher-order extension of the recent path-sum symbolic representation, used for both specification and automation. To illustrate the opportunity of Qbricks, we implement the first verified parametric implementations of several famous and non-trivial quantum algorithms, including the quantum part of Shor integer factoring (Order Finding - Shor-OF), quantum phase estimation (QPE) - a basic building block of many quantum algorithms, and Grover search. These breakthroughs were amply facilitated by the specification and automated deduction principles introduced within Qbricks.
△ Less
Submitted 26 July, 2020; v1 submitted 12 March, 2020;
originally announced March 2020.
-
Deductive Proof of Ethereum Smart Contracts Using Why3
Authors:
Zeinab Nehai,
François Bobot
Abstract:
A bug or error is a common problem that any software or computer program may encounter. It can occur from badly writing the program, a ty** error or bad memory management. However, errors can become a significant issue if the unsafe program is used for critical systems. Therefore, formal methods for these kinds of systems are greatly required. In this paper, we use a formal language that perform…
▽ More
A bug or error is a common problem that any software or computer program may encounter. It can occur from badly writing the program, a ty** error or bad memory management. However, errors can become a significant issue if the unsafe program is used for critical systems. Therefore, formal methods for these kinds of systems are greatly required. In this paper, we use a formal language that performs deductive verification on an Ethereum Blockchain application based on smart contracts, which are self-executing digital contracts. Blockchain systems manipulate cryptocurrency and transaction information. Therefore , if a bug occurs in the blockchain, serious consequences such as a loss of money can happen. Thus, the aim of this paper is to propose a language dedicated to deductive verification, called Why3, as a new language for writing formal and verified smart contracts, thereby avoiding attacks exploiting such contract execution vulnerabilities. We first write a Why3 smart contracts program; next we formulate specifications to be proved as absence of RunTime Error properties and functional properties, then we verify the behavior of the program using the Why3 system. Finally we compile the Why3 contracts to the Ethereum Virtual Machine (EVM). Moreover, we give a set of generic mathematical statements that allows verifying functional properties suited to any type of smart contracts holding cryptocurrency, showing that Why3 can be a suitable language to write smart contracts. To illustrate our approach, we describe its application to a realistic industrial use case.
△ Less
Submitted 23 August, 2019; v1 submitted 25 April, 2019;
originally announced April 2019.
-
CDCL-inspired Word-level Learning for Bit-vector Constraint Solving
Authors:
Zakaria Chihani,
François Bobot,
Sébastien Bardin
Abstract:
The theory of quantifier-free bit-vectors (QF_BV) is of paramount importance in software verification. The standard approach for satisfiability checking reduces the bit-vector problem to a Boolean problem, leveraging the powerful SAT solving techniques and their conflict-driven clause learning (CDCL) mechanisms. Yet, this bit-level approach loses the structure of the initial bit-vector problem. We…
▽ More
The theory of quantifier-free bit-vectors (QF_BV) is of paramount importance in software verification. The standard approach for satisfiability checking reduces the bit-vector problem to a Boolean problem, leveraging the powerful SAT solving techniques and their conflict-driven clause learning (CDCL) mechanisms. Yet, this bit-level approach loses the structure of the initial bit-vector problem. We propose a conflict-driven, word-level, combinable constraints learning for the theory of quantifier-free bit-vectors. This work paves the way to truly word-level decision procedures for bit-vectors, taking full advantage of word-level propagations recently designed in CP and SMT communities.
△ Less
Submitted 28 June, 2017;
originally announced June 2017.
