Download as KEY, PPTX
Uploaded byHiroki Mizuno
「Frama-Cによるソースコード検証」 (mzp)
This document discusses using the Frama-C framework to formally verify C and C++ code. It provides examples of using Frama-C to verify functions that find the minimum of integer values, including abs(), min(), and min3(). Specifications for these functions are written using the ACSL specification language. Frama-C is then used to prove that the implementations satisfy the specifications. The document also discusses how concepts from Frama-C like LE (less than or equal) can be mapped to similar concepts in languages like Coq that are used for formal verification.
More Related Content
Similar to 「Frama-Cによるソースコード検証」 (mzp)
「Frama-Cによるソースコード検証」 (mzp)
- 1. 2011/05/14 Boost. Frama-C mzp / 1
- 2. mzp / SE > ocaml-nagoya > ProofCafe > Scala 2
- 4. 2/26 Ruby 02 4
- 5. Reject 5
- 6. Reject → 5
- 7. @bleis bf SQL @sunflat Amazon EC2 @yoya PHP: ZendEngine @terurou CommonJS @nari3 GC @mallowlabs AsakusaSattelite @yoshihiro503 Coq @mzp @wof_moriguchi F# @keigoi ocamljs ocaml android ( ) @osiire GADT @kaizen_nagoya XYZ @dico_leque Meta-objective Lisp 6
- 8. @bleis bf SQL @sunflat Amazon EC2 @yoya PHP: ZendEngine @terurou CommonJS @nari3 GC @mallowlabs AsakusaSattelite @yoshihiro503 Coq @mzp ! @wof_moriguchi F# @keigoi ocamljs ocaml android ( ) @osiire GADT @kaizen_nagoya XYZ @dico_leque Meta-objective Lisp 7
- 9.
- 10.
- 12. :min() min() 2 ← 11
- 13. template ≦ OK > (structual subtype) template <class T> T min(T x, T y) { return (x <= y) ? x : y; } 12
- 14. auto concept Le<classT> { bool operator<=(T, T); } template <class T> requires Le<T> T min(T x, T y) { return x <= y ? x : y; } 13
- 15. // int BOOST_CHECK_EQUAL( min(1,2), 1 ); BOOST_CHECK_EQUAL( min(2, 1), 1 ); BOOST_CHECK_EQUAL( min(3, 3), 3 ); // dobule BOOST_CHECK_EQUAL( min(1., 2.), 1. ); BOOST_CHECK_EQUAL( min(2., 1.), 1. ); 14
- 16. ... 3 ← 15
- 17. 1 min ≦ OK template <class T> requires Le<T> T min3(T x, T y, T z) { return min(x, min(y, z)); } 16
- 18. // int BOOST_CHECK_EQUAL( min3(1,2,3), 1 ); BOOST_CHECK_EQUAL( min3(2, 1,3), 1 ); BOOST_CHECK_EQUAL( min3(3, 2,1), 1 ); // dobule BOOST_CHECK_EQUAL( min3(1., 2.,4.), 1. ); BOOST_CHECK_EQUAL( min3(2., 1.,4.), 1. ); 17
- 19.
- 20. “ ”: int int ≦ :x≦y z≦w (x,z) ≦ (y,w) &'( !"#"$ ← !"#%$ !%#"$ )*( !%#%$ 19
- 21. “ ”: int int ≦ :x≦y z≦w (x,z) ≦ (y,w) &'( !"#"$ ← !"#%$ !%#"$ )*( !%#%$ 19
- 22. ≦ OK ← > :x≦x > :x≦y y≦z x≦z ↑ 20
- 23. > ≦ bool min,min3 ↑ 21
- 24.
- 25.
- 27. Frama-C[1] C > Value Analysis,Effects Analysis, etc 24
- 28. C → Why→ > Alt-Ergo: ← > Coq: ← > ...and more ACSL > ACSL = ANSI/ISO C Specification Language !"#$#%& '() *+,%-"./ 25 00&/1
- 29. : abs() abs : 0 ACSL //@ ensures result >= 0; int abs (int i) { return i < 0 ? -i : i; } 26
- 30. $ frama-c -jessieabs.c 27
- 31. $ frama-c -jessieabs.c 27
- 32. $ frama-c -jessieabs.c 27
- 33. $ frama-c -jessieabs.c ! 27
- 34. $ frama-c -jessieabs.c INT_MIN ! 27
- 35. requires INT_MIN //@ requires i > -2147483648; //@ ensures result >= 0; int abs (int i) { return i < 0 ? -i : i; 28
- 36.
- 37. Frama-C C++ C C++ > Frama-C 30
- 38. : LE ≦ → LE >C ACSL /*@ axiomatic order { predicate LE(T x, T y); } */ 31
- 39. Frama-C min,min3 C++ Frama-C T → void* → > typedef void* T; bool leq(T x, T y) { return true; } 32
- 40. leq leq : LE > leq(x,y) true LE(x,y) > leq(x,y) false LE(y, x) /*@ ensures (¥result == true ==> LE(x,y)) && (¥result == false ==> LE(y,x)); */ bool leq(T x, T y){ ... } 33
- 41. min leq min x,y /*@ ensures LE(¥result, x) && LE(¥result, y); */ T min(T x,T y){ return leq(x,y) ? x : y; } 34
- 42.
- 43.
- 44. /*@ axiomatic order{ predicate LE(T x, T y); axiom refl : ¥forall T x; LE(x,x); ← 37
- 45. min3 min3 : x,y,z /*@ ensures LE(result, x) && LE(result, y) && LE(result, z); */ T min3(T x,T y,T z){ return min(x, min(y,z)); 38
- 46.
- 47. > Coq → LE( , min(y,z)) LE(min(y,z), y) LE( , y) 40
- 48. /*@ axiomatic order{ predicate LE(T x, T y); axiom refl : ¥forall T x; LE(x,x); axiom trans: forall T x,T y,T z; LE(x,y) ==> LE(y,z) ==> LE(x,z); ← 41
- 49. Frama-C min,min3 42
- 50. :ProofSummit 9/25( ) 10:00 17:00 @ http://bit.ly/proofsummit Coq,Agda2 43