• Document: SuSLik: synthesis of safe pointer-manipulating programs Nadia Polikarpova joint work with Ilya Sergey (Yale-NUS) follow along 2 pointer-manipulating programs operating
  • Size: 1.18 MB
  • Uploaded: 2020-11-30 01:03:41
  • Status: Successfully converted


Some snippets from your converted document:

SuSLik: synthesis of safe pointer-manipulating programs Nadia Polikarpova joint work with Ilya Sergey (Yale-NUS) follow along https://github.com/TyGuS/suslik-tutorial 2 pointer-manipulating programs network / security operating systems browsers protocols ☺ efficient  hard to write  memory safety bugs 3 how to make them safe? write in a write in C, high-level verify in Coq language ☺ easy to write  hard to write  have to rewrite everything ☺ backwards compatible 4 program synthesis to the rescue specification code ☺ easy to write  verbose ☺ efficient  unstructured ☺ backwards compatible  pointers & aliasing ☺ provably memory-safe 5 SuSLik (Synthesis using Separation Logik) the SuSLik approach separation deductive logic specification synthesis code ☺ reasoning about ☺ uses specs pointers & aliasing to guide synthesis 7 this tutorial 1. example: swap a taste of SuSLik 2. intro to separation logic reasoning about pointer-manipulating programs 3. deductive synthesis from SL specifications to programs 8 this tutorial 1. example: swap 2. intro to separation logic 3. deductive synthesis 9 example: swap Swap values of two distinct pointers void swap(loc x, loc y) 10 example: swap in separation logic: start state: A B {x↦A*y↦B} precondition x y separately void swap(loc x, loc y) end state: B A {x↦B*y↦A} postcondition x y ghost variables 11 demo 1: swap Swap values of two distinct pointers void swap(loc x, loc y) 12 {x↦A*y↦B} ?? {x↦B*y↦A} let a1 = *x; { x ↦ a1 * y ↦ B } ?? { x ↦ B * y ↦ a1 } let a1 = *x; let b1 = *y; { x ↦ a1 * y ↦ b1 } ?? { x ↦ b1 * y ↦ a1 } let a1 = *x; let b1 = *y; *x = b1; { x ↦ b1 * y ↦ b1 } ?? { x ↦ b1 * y ↦ a1 } let a1 = *x; let b1 = *y; *x = b1; *y = a1; { x ↦ b1 * y ↦ a1 } ?? same { x ↦ b1 * y ↦ a1 } let a1 = *x; let b1 = *y; *x = b1; *y = a1; void swap(loc x, loc y) { let a1 = *x; let b1 = *y; *x = b1; *y = a1; } exercise 1: rotate three start state: A B C x y z void rotate(loc x, loc y, loc z) end state: C A B x y z 20 this tutorial 1. example: swap 2. intro to separation logic 3. deductive synthesis 21 separation logic (SL) Hoare logic “about the heap” 22 separation logic (SL) SL assertions {P} c {Q} program starting in a state that satisfies P program c will execute without memory errors, and upon its termination the state will satisfy Q 23 this tutorial 1. example: swap 2. intro to separation logic 2.1. programs and assertions 2.2. inductive predicates 2.3. specifying data transformations 3. deductive synthesis 24 separation logic (SL) {P} c {Q} program 25 programs do nothing skip 26 programs offset (natural number) do nothing skip read from heap let y = *(x + n) variables 27 programs do nothing skip read from heap let y = *(x + n) write to heap *(x + n) = e expression (arithmetic, boolean) 28 programs do nothing skip read from heap let y = *(x + n) write to heap *(x + n) = e allocate block let y = malloc(n)

Recently converted files (publicly available):