DOC PREVIEW
Berkeley COMPSCI 161 - Program Verification & Other Types of Vulnerabilities

This preview shows page 1-2-3 out of 9 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 9 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 9 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 9 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 9 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

1Program Verification & Other Types of VulnerabilitiesDawn [email protected]• Memory-safety vulnerabilities• Runtime detection• Fuzzing for bug finding– Blackbox fuzzing– Whitebox fuzzing3This Class• Program verification• Other types of vulnerabilities4Static Analysis• Instead of running the code to detect attacks or find bugs, we statically analyze code• Simple pattern match:– Whether program uses unsafe APIs: gets, sprintf, etc.• Simple checks:– E.g., variable use before def or initialization• More sophisticated analysis– E.g., potential array-out-of-bounds check• Many tools available– Open source: http://en.wikipedia.org/wiki/List_of_tools_for_static_code_analysis– Commercial tools: Coverity, Fortify, etc.5Program Verification• Can we prove a program free of buffer overflows?• How to prove a program free of buffer overflows?– Precondition– Postcondition– Loop invariants6Precondition• Functions make certain assumptions about their arguments– Caller must make sure assumptions are valid– These are often called preconditions• Precondition for f() is an assertion (a logical proposition) that must hold at input to f()– Function f() must behave correctly if its preconditions are met– If any precondition is not met, all bets are off• Caller must call f() such that preconditions true – an obligation on the caller, and callee may freely assume obligation has been met• The concept similarly holds for any statement or block of statements7Simple Precondition Example• int deref(int *p) {return *p;}• Unsafe to dereference a null pointer– Impose precondition that caller of deref() must meet: p ≠ NULL holds at entrance to deref()• If all callers ensure this precondition, it will be safe to call deref()• Can combine assertions using logical connectives (and, or, implication)– Also existentially and universally quantified logical formulas8Another Example• int sum(int *a[], size_t n) {int total = 0, i;for (i=0; i<n; i++)total += *(a[i]);return total;}• Precondition: – a[] holds at least n elements– Forall j.(0 ≤ j < n) → a[j]≠NULL9Postcondition• Postcondition for f() is an assertion that holds when f() returns–f() has obligation of ensuring condition is true when it returns– Caller may assume postcondition has been established by f()• Example:void *mymalloc(size_t n) {void *p = malloc(n);if (!p) {perror("Out of memory");exit(1);}return p;}• Post condition: retval != NULL10Proving Precondition→Postcondition• Given preconditions and postconditions– Which specifies what obligations caller has and what caller is entitled to rely upon• Verify that, no matter how function is called, if precondition is met at function’s entrance, then postcondition is guaranteed to hold upon function’s return – Must prove that this is true for all inputs– Otherwise, you’ve found a bug in either specification (preconditions/postconditions) or implementation11Proving Precondition→Postcondition• Basic idea:– Write down a precondition and postcondition for every line of code– Use logical reasoning• Requirement:– Each statement’s postcondition must match (imply) precondition of any following statement– At every point between two statements, write down invariant that must be true at that point» Invariant is postcondition for preceding statement, and precondition for next one12Example• Easy to tell if an isolated statement fits its pre- and post-conditions• postcondition for “v=0;”is –v=0 (no matter what the precondition is)– Or, if precondition for “v=v+1;”is v≥5, then a valid postcondition is» v≥6• If precondition for “v=v+1;”is w≤100, then a valid postcondition is –w≤100– Assuming v and w do not alias13Loop Invariant• An assertion that is true at entrance to the loop, on any path through the code– Must be true before every loop iteration» Both a pre- and post-condition for the loop body• Example: Factorial function code– /* Requires: n >= 1 */int fact(int n) {int i, t;i = 1;t = 1;while (i <= n) {t *= i;i++;}return t;}– Prerequisite: input must be at least 1 for correctness– Prove: value of fact() is always positive14Verifying Invariant Correctness• /* Requires: n >= 1Ensures: retval >= 0 */int fact(int n) {int i, t; /* n>=1 */i = 1; /* n>=1 && i==1 */t = 1; /* n>=1 && i==1 && t==1 */while (i <= n) {/* 1<=i && i<=n && t>=1 <-- loop invariant */t *= i; /* 1<=i && i<=n && t>=1 */i++; /* 2<=i && i<=n+1 && t>=1 */} /* i>n && t>=1 */return t;}• Easy if we examine each step:– Function’s precondition implies invariant at function body start– Invariant at end of function body implies function’s postcondition– If each statement matches invariant immediately before and after it, everything’s OK• That leaves the loop invariant…15Verifying the Loop Invariant• Loop invariant: 1<=i && i<=n && t>=1• Prove it is true at start of first loop iteration– Follows from: » n≥1 ∧ i=1 ∧ t=1 → 1≤i≤n ∧ t≥1» if i=1, then certainly i≥1 • Prove that if it holds at start of any loop iteration, then it holds at start of next iteration (if there’s one)– True, since invariant at end of loop body 2≤i≤n+1 ∧ t≥1 and loop termination condition i≤n implies invariant at start of loop body 1≤i≤n ∧ t≥1• Follows by induction on number of iterations that loop invariant is always true on entrance to loop body– Thus, fact() will always make postcondition true, as precondition is established by its caller16Function Post-/Pre-Conditions• Any time we see a function call, we have to verify that its precondition will be met– Then we can conclude its postcondition holds and use this fact in our reasoning• Annotating every function with pre- and post-conditions enables modular reasoning– Can verify function f() by looking only its code and the annotations on every function f() calls» Can ignore code of all other functions and functions called transitively– Makes reasoning about f() an almost purely local activity17Documentation• Pre-/post-conditions serve as useful documentation– To invoke Bob’s code, Alice only has to look at pre- and post-conditions – she doesn’t need to look at or understand his code• Useful way to coordinate activity between multiple programmers:– Each module assigned to one programmer, and


View Full Document

Berkeley COMPSCI 161 - Program Verification & Other Types of Vulnerabilities

Documents in this Course
Rootkits

Rootkits

11 pages

Load more
Download Program Verification & Other Types of Vulnerabilities
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Program Verification & Other Types of Vulnerabilities and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Program Verification & Other Types of Vulnerabilities 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?