SymDiff: A Differential Program Verifier

SymDiff is a platform that leverages program verification to analyze program differences, focusing on differential verification to verify properties of program variances rather than the program itself. The architecture, language subset, and modeling imperative programs/heaps are key components discussed. Differential specifications and their applications are highlighted, showcasing its potential in program evolution and compilers.

• SymDiff
• Program Verifier
• Differential Verification
• Software Engineering
• Program Evolution

nev_can Follow

Uploaded on Sep 10, 2024 | 2 Views

Download Presentation

Please find below an Image/Link to download the presentation.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

Presentation Transcript

1. SymDiff: A differential program verifier Shuvendu Lahiri Research in Software Engineering (RiSE), Microsoft Research, Redmond, WA USA Workshop on Program Equivalence (April 2016)

2. What is SymDiff? A platform for Leveraging and extending program verification to reason about program differences http://research.microsoft.com/symdiff Contributors C. Hawblitzel, K. McMillan, O. Strichman, Z. Rakamaric, S. He, Interns: R. Sharma, M. Kawaguchi, H. Rebelo, R. Sinha, N. Partush, A. Gyori, 2

3. Differential verification Verifying properties of program differences instead of the program itself Motivations No specs! Proving assertions statically is harder (program-specific invariants, environment modeling, ..) Applications Program evolution Compilers (equivalence preserving, approximate) Comparing independent implementations 3

4. SymDiff architecture Language agnostic: relies on translators from C/C#/Java/x86 to Boogie (bpl) P1.bpl Invariant inference Product P1P2.bpl P2.bpl P1P2.bpl + invs Diff spec Boogie program verifier+ Z3 4

5. Language Subset of Boogie(an intermediate verification language) [FMCO 05] Commands x := E assert E assume E S;T goto L1, L2, Ln //non-deterministic jump to labels call x,y := Foo(e1,e2,..) //procedure call Loops encoded as tail-recursive procedures Can encode arrays using SMT theory of arrays (sel/upd) x[e] sel(x, e) x[y] := z x := upd(x, y, z) x == y i. sel(x,i) == sel(y,i) 5

6. Modeling imperative programs/heaps Various translators to Boogie: C (HAVOC/SMACK/VCC/..), JAVA (Joogie/..), C# (BCT) E.g., C Heap modeling in HAVOC [CHLQ, POPL 09] A pointer is represented as an integer (int) One heap map per scalar/pointer structure field and pointer type struct A { int f; int g;} x; Mem_A_f : [int]int Mem_A_g : [int]int Simple example C code x->f = 1; Boogie Mem_A_f[x + Offset(f,A)] := 1; 6

7. Differential specs: mutual summaries void F1(int x1){ if(x1 < 100){ g1 := g1 + x1; F1(x1 + 1); }} void F2(int x2){ if(x2 < 100){ g2 := g2 + 2* x2; F2(x2 + 1); }} MS(F1, F2): (x1 = x2 && g1 <= g2 && x1 >= 0) ==> g1 <= g2 A specification over the I/O vocabulary of (F1,F2) Inputs: parameters, globals (g). Outputs: return values, next state of globals (g ). [Hawblitzel, Kawaguchi, Lahiri, Rebelo CADE 13] 7

8. And now... verification. Differential verification single-program verification Leverage existing verification machinery: VC generation, SMT solvers Invariant inference to infer intermediate specifications A novel product (P1 x P2) construction [FSE 13] Allows Interprocedural reasoning Synchronizes at procedure boundaries only Can map one procedure to many procedures 8

9. The product program f1 Instrument calls proc f1(x1): r1 modifies g1 { s1; L1: w1 := call h1(e1); t1 } f2 Instrument calls proc f2(x2): r2 modifies g2 { s2; L2: w2 := call h2(e2); t2 } Replay, constrain, restore 9

10. Property of the product Let p1_p2 be the product of (p1, p2) Theorem: If S_p1_p2 is a summary of p1_p2, then it is a mutual summary of (p1, p2) Aids in differential specification A specification of the summary S_p1_p2 (e.g. partial equivalence) can be added as a postcondition of p1_p2 More importantly, aids differential invariant inference Can perform analysis on program P1xP2 to infer sound mutual summaries of (P1, P2) 10

11. Automatic differential invariant inference Performing invariant inference on the product program Experience with Duality (infers invariants) Diverges e.g., ((?1= 0 ?1= 1) (?1= 1 ?2= 2) ) instead of (?1< ?2) Current approach is based on predicate abstraction Infer Boolean combination of predicates, or Houdini: Conjunction over a predefined set of predicates Automatically provide all simple differential predicates: x1 x2, where x1 in p1, x2 in p2, {=, , , } 11

12. Applications (1 / 3) Equivalence checking Compiler translation validation [CADE 13] Cross-version compiler validation by comparing binaries [FSE 13] 12

13. Example (equivalence checking) f1(n) { if (n == 0) { return 1; } else { return n * f1(n - 1); } } main(n) {return f1(n);} involves non-trivial diff specs user only provides predicate (a2*r1 == r2 ) f2(n, a) { if (n == 0) { return a; } else { return f2(n - 1, a * n); } } main(n) {return f2(n,1);} MS(f1, f2): (n1 == n2 a2*r1 == r2 ) Spec MS(main1, main2) = (n1 == n2 r1 == r2 ) 13

14. Applications (2 / 3) Differential assertion checking [FSE 13] 14

15. Differential Assertion Checking (DAC) Lahiri et al. FSE 13, Joshi, Lahiri, Lal POPL 12 Correctness Relative correctness An input that can* satisfy p, cannot fail p . Note: asymmetric check How? Replace assert A with ok := ok && A; Write a mutual summary: MS(f1,f2) = ((i1==i2 && ok1 ) ==> ok2 )) * Nondeterminism 15

16. DAC application: verifying bug fixes Does a fix inadvertently introduce new bugs? Verisec suite: snippets of open source programs which contain buffer overflow vulnerabilities, and corresponding patched versions. Relative memory safety (e.g. buffer overflow) checking Snippets from apache, madwifi, sendmail etc. Verified several bug fixes using automatic differential invariant inference 16

17. Example: DAC int main_buggy() { fb := 0; while(c1=read()!=EOF) { fbuf[fb] = c1; fb++; } } int main_patched() { fb := 0; while(c1=read()!=EOF) { fbuf[fb] = c1; fb++; if(fb >= MAX) fb = 0; } } manual preconditions Differential loop invariant:fb2 fb1 Buffer Overflow Can verify (relative) memory safety automatically, without 17

18. Applications (3/3) Current research: Verifying approximate transformations Preserve assertions, termination and accuracy [w/ Rakamaric, He] Semantic change impact analysis Injecting change semantics into a dataflow-based taint analysis [w/ Partush, Gyori] 18