formal_methods.md 2.13 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15

<!-- Link definitions  -->
[Alt-Ergo]: https://alt-ergo.ocamlpro.com
[Why3]: http://why3.lri.fr
[Frama-C]: https://frama-c.com
[SPARK]: https://www.adacore.com/sparkpro
[Common Criteria]: https://www.commoncriteriaportal.org/
[B]: https://www.atelierb.eu/
[CEA List]: http://www-list.cea.fr/
[MERCE]: https://www.mitsubishielectric-rce.eu/
[INRIA]: https://www.inria.fr/fr
[Adacore]: https://www.adacore.com/
[TrustInSoft]: https://trust-in-soft.com/
[Dolmen]: https://github.com/Gbury/dolmen

16 17
# Formal Methods

18

19
<!-- [JB] Only content for now. Maybe add an intro ? -->
20

21 22
## Alt-Ergo

23 24 25
[Alt-Ergo] is an open-source automatic solver
based on Satisfiability Modulo Theories (SMT). Successfully designed for 
proving formulas generated in the
26 27 28
context of deductive program verification.

It is mostly used as a back-end of different program verification tools via
29 30 31
the [Why3] platform like [Frama-C]
for C or [SPARK] for Ada. [Alt-Ergo] is also used
to prove formulas issued from [B] modelizations and from cryptographic protocols
32 33 34 35 36 37 38 39 40 41
verification. 

## Program Verification

We developped several static analysis enforcing security or safety properties
in various languages:
- safety requirements in C <!-- [JB] can we mention MERCE and/or the related project? -->
- OCaml exceptions tracking <!-- [JB] add SecureOCaml FUI link? -->
- reaching unspecified or breaking invariant states in transition system based languages <!-- [JB] GEHC is under NDA so we can't talk explicitly about it but we may link to mikino/verification for dummies. -->

42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64
## Certification

High assurance level in [Common Criteria] certification implies the formalization
of at least the security policy model corresponding to the family SPM. Such 
formalization is usually expensive and subcontracting it lower both the risk 
and costs.

Our experienced R&D team can deal with it and help your products reaching the
EAL 6 or 7 certification.

## Partnership

We are involved in formal methods related partnership:
- [INRIA]
- [CEA List]
- [MERCE]
- [Adacore]
- [TrustInSoft]
- <!-- [JB] More ?-->

In addition, we contribute to open-source tooling:
- [Dolmen]: a generic front-end for solvers
- <!-- [JB] What else ? -->