CMU 15-414 Bug Catching: Automated Program Verification and Testing Abstract Interpretation9 Nov 2011Soonho [email protected], Motivation, and Big Picture“Software is Hard.”“Software is Hard.”- Donald E. KnuthSoftware Verification is Harder:Software Verification is Harder:“Any non-trivial property about the language recognized by a Turing machine is undecidable.”- Rice’s eorem• Large / unbounded base types: int, float, string • User-defined types / classes • Pointers/aliasing + unbounded #’s of heap allocated cells • Procedure calls / recursion / calls through pointers / dynamic method lookup / overloading • Concurrency + unbounded #’s of threads• Templates / generics / include files • Interrupts / exceptions / callbacks • Use of secondary storage: files, databases • Absent source code for: libraries, system calls, mobile code • Esoteric features: continuations, self-modifying code • Size (e.g., MS Word = 1.4 MLOC)“In the development of the understanding of complex phenomena, the most powerful tool available to the human intellect is abstraction.”- C. A. R. Hoare“In the development of the understanding of complex phenomena, the most powerful tool available to the human intellect is abstraction.”- C. A. R. Hoare“e purpose of abstraction is not to be vague, but to create a new semantic level in which one can be absolutely precise.”- Edsger W. DijkstraWhat does Abstraction mean to Model Check Software?ConcreteModelAbstractModelWhat do we expect from Abstraction?ConcreteModelAbstractModelˆM|=ˆ () M |= What do we expect from Abstraction?ConcreteModelAbstractModelˆM|=ˆ =)M|= Preservation eorem (Clarke, Grumberg, Long) If property(ACTL*) holds on abstract model, it holds on concrete modelWhat do we expect from Abstraction?ConcreteModelAbstractModelˆM 6|=ˆ =) M 6|= What do we expect from Abstraction?ˆM 6|=ˆ =) M 6|= REDGOAG AF ˆMMAbstractModelConcreteModelAG AF REDSpurious Counterexample: <RED> <GO> <GO> <GO> ...Artifact of the abstraction!What we should expect from Abstraction:ConcreteModelAbstractModelˆM|=ˆ =)M|= ˆM 6|=ˆ =) M 6|= Informal Introduction to Abstract Interpretation with Examples?371 * 285 * 124 * 890 * 212 * 489 * 721 = even number371 * 285 * 124 * 890 * 212 * 489 * 721 -----> 872188680940768800F?371 * 285 * 124 * 890 * 212 * 489 * 721 = even numberZConcrete Domain371 * 285 * 124 * 890 * 212 * 489 * 721 -----> 872188680940768800 O * O * E * E * E * O * O -----> Even!↵F?371 * 285 * 124 * 890 * 212 * 489 * 721 = even numberZConcrete DomainAbstract Domain{O, E }371 * 285 * 124 * 890 * 212 * 489 * 721 -----> 872188680940768800 O * O * E * E * E * O * O -----> Even!↵↵↵↵↵↵↵↵F?371 * 285 * 124 * 890 * 212 * 489 * 721 = even numberZConcrete DomainAbstract Domain{O, E }371 * 285 * 124 * 890 * 212 * 489 * 721 -----> 872188680940768800 O * O * E * E * E * O * O -----> Even!↵↵↵↵↵↵↵↵FˆF?371 * 285 * 124 * 890 * 212 * 489 * 721 = even numberZConcrete DomainAbstract Domain{O, E }? 35 * 24 * 31 * 89 * 21 * 48 * 71 = 6n35 * 24 * 31 * 89 * 21 * 48 * 71 -----> 165863134080 X * 6 * X * X * X * 6 * X -----> Divided by 6!↵F? 35 * 24 * 31 * 89 * 21 * 48 * 71 = 6nZConcrete Domain35 * 24 * 31 * 89 * 21 * 48 * 71 -----> 165863134080 ? * 6 * ? * ? * ? * 6 * ? -----> 6 = Divided by 6!↵↵↵↵↵↵↵↵FˆF? 35 * 24 * 31 * 89 * 21 * 48 * 71 = 6nZConcrete DomainAbstract Domain{6, ?}35 * 24 * 31 * 89 * 21 * 48 * 71 -----> 165863134080 ? * 6 * ? * ? * ? * 6 * ? -----> 6 = Divided by 6!↵↵↵↵↵↵↵↵FˆF? 35 * 24 * 31 * 89 * 21 * 48 * 71 = 6nZConcrete DomainAbstract Domain{6, ?}Result of Abstract execution “6” andConcrete execution “6” coincide!?371 * 285 * 124 * 890 * 212 * 489 * 721 = 6n371 * 285 * 124 * 890 * 212 * 489 * 721 -----> 872188680940768800 ? * ? * ? * ? * ? * ? * ? -----> ? <> 6!↵F?371 * 285 * 124 * 890 * 212 * 489 * 721 = 6nZConcrete Domain371 * 285 * 124 * 890 * 212 * 489 * 721 -----> 872188680940768800 ? * ? * ? * ? * ? * ? * ? -----> ? <> 6!↵↵↵↵↵↵↵↵FˆF?371 * 285 * 124 * 890 * 212 * 489 * 721 = 6nZConcrete DomainAbstract Domain{6, ?}371 * 285 * 124 * 890 * 212 * 489 * 721 -----> 872188680940768800 ? * ? * ? * ? * ? * ? * ? -----> ? <> 6!↵↵↵↵↵↵↵↵FˆF?371 * 285 * 124 * 890 * 212 * 489 * 721 = 6nZConcrete DomainAbstract Domain{6, ?}Result of Abstract execution “?” andConcrete execution “6” does not coincide!371 * 285 * 124 * 890 * 212 * 489 * 721 -----> 872188680940768800 ? * ? * ? * ? * ? * ? * ? -----> ? <> 6!↵↵↵↵↵↵↵↵FˆF?371 * 285 * 124 * 890 * 212 * 489 * 721 = 6nZConcrete DomainAbstract Domain{6, ?}It’s OK! Because ‘?’ means “WE DON’T KNOW”!Our abstract execution is still sound, but not precise enough!Formal Introduction to Abstract Interpretation with Examples{}AnyNoneZeroNegPosConcrete Domain :DAbstract Domain :ˆDZ(2Z, ✓)(Sign, v){0}{-1} {1}{-214987, -1, 0, 1, 38134729}{-214987, -1}{1, 38134729}{n | n<0}{n | n>0}{}AnyNoneZeroNegPosConcrete Domain :DAbstract Domain :ˆDZ(2Z, ✓)(Sign, v){0}{-1} {1}{-214987, -1, 0, 1, 38134729}{-214987, -1}{1, 38134729}Need to have abstraction function( ) and concretization function ( )to give a meaning to an Abstract Domain↵ˆD{n | n<0}{n | n>0}{}AnyNoneZeroNegPosConcrete Domain :DAbstract Domain :ˆDZ(2Z, ✓)(Sign, v){0}{-1} {1}{-214987, -1, 0, 1, 38134729}{-214987, -1}{1, 38134729}Need to have abstraction function( ) and concretization function ( )to give a meaning to an Abstract Domain↵ˆD↵↵↵↵↵↵{n | n<0}{n | n>0}{}AnyNoneZeroNegPosConcrete Domain :DAbstract Domain :ˆDZ(2Z, ✓)(Sign, v){0}{-1} {1}{n | n<0}{n | n>0}{-214987, -1, 0, 1, 38134729}{-214987, -1}{1, 38134729}Need to have abstraction function( ) and concretization function ( )to give a meaning to an Abstract Domain↵ˆDWhat is the general condition that and should satisfy? ~ Galois Connection.↵↵8x 2