#1Program analysis for security:Making it scaleDavid WagnerU.C. BerkeleyWork by Hao Chen, Karl Chen, Rob Johnson, Ben Schwarz,and Jeremy Lin, Geoff Morrison, David Schultz, Jacob West#2• Wrapping up the MOPS project• End-of-project experimental evaluation• Lessons• Verification of security properties via type inference• Modular analysis• Preliminary results: user/kernel, format strings Outline#3• Pushdown model checking of C source code• Security properties expressed as finite state automataRefresher on MOPSstrncpy(d,s,n)otherd[n-1] = ’\0’;Example: A simple FSA to detect misuse of strncpy( ).Error state indicates possible failure to null-terminate d.(Real property is much more complex: many ways to terminate;pre-termination vs. post-termination; delayed termination.)#4• Canonical example of a TOCTTOU vulnerability:if (access(pathname, R_OK) == 0) fd = open(pathname, O_RDONLY);• Notice: not an atomic operation!• Bug: Permissions may change between access() & open()• Attacker can arrange for this to happen in an attackTOCTTOU (time-of-check to time-of-use)check(x)use(x)check = { access, lstat, stat, readlink, statfs }use = { chmod, open, remove, unlink, mount, link, mkdir, rmdir … }#5• Temporary file creation requires special care: 1) unguessable filename; 2) safe permissions; 3) file ops should use fd, not filename (TOCTTOU)Insecure temporary file creation/usemkstemp(x)fileop(x)fileop(x) = { open(x), chmod(x), remove(x), unlink(x) … }{ tmpnam(), tempnam(), mktemp(), tmpfile() }#6• Experiment: Analyze an entire Linux distribution• Redhat 9, all C packages (732 pkgs, ~ 50 MLOC)• Security analysis at an unprecedented scale• Team of 4 manually examined 900+ warnings• 1 grad student; 3 undergrads new to MOPS• Exhaustive analysis of TOCTTOU, tmpfile, others; statistical sampling of strncpy• Laborious: multiple person-months of effort• Found 79 new security holes in Linux appsMOPS in the large79+1597Total~ 5-10%(unknown)668strncpy35%34108temporary files5%41790TOCTTOUBug ratioReal bugsWarningsSecurity Property#7• Unexpectedly, most real bugs were local• False alarm rate high. Doing better requires deeper modeling of OS/filesystem semantics.• Path sensitivity only good for ≤ 2x improvement• Many non-bugs were still very interesting (represented fragile assumptions about environment)• Engineering for analysis at scale is highly non-trivial• Good UI, explanation of errors is critical• Build integration so important — and so hard — that we re-implemented it no less than four times• But worth it: Large-scale experiments incredibly valuable• Tech. transfer: techniques being adopted in commercial security code scanning toolsLessons & surprises from the MOPS effort#8Bug #1: “zip”d_exists = (lstat(d, &t) == 0);if (d_exists) { /* respect existing soft and hard links! */ if (t.st_nlink > 1 ||(t.st_mode & S_IFMT) == S_IFLNK) copy = 1; else if (unlink(d)) return ZE_CREAT;}... eventually writes new zipfile to d ...Pathname from cmd line#9Bug #2: “ar”exists = lstat (to, &s) == 0; if (! exists || (!S_ISLNK (s.st_mode) && s.st_nlink == 1)){ ret = rename (from, to); if (ret == 0) { if (exists) { chmod (to, s.st_mode & 0777); if (chown (to, s.st_uid, s.st_gid) >= 0) chmod (to, s.st_mode & 07777); } }}#10Bug #3static void open_files() { int fd; create_file_names(); if (input_file == 0) { input_file = fopen(input_file_name, "r"); if (input_file == 0) open_error(input_file_name); fd = mkstemp(action_file_name); if (fd < 0 || (action_file = fdopen(fd, "w")) == NULL) { if (fd >= 0) close(fd); open_error(action_file_name); }}void open_error(char *f) { perror(f); unlink(action_file_name); exit(1);}#11State of the art• Research direction: verify absence of data-driven attacks, using type inferenceCurrent researchBest-effortbugfindingSoundnessmanual audits,grepVerify absenceof classes of bugsfull programverification#12State of the art• Research direction: verify absence of data-driven attacks, using type inferenceBest-effortbugfindingSoundnessmanual audits,grepVerify absenceof classes of bugsfull programverificationCurrent focusCurrent research#13• Q: Why is writing secure code hard? A: Secure programs must handle untrusted data securely, and must get it right every single time.• Focus area: input validation• Untrusted data should be sanitized before it is used at any trusting consumer• Defends against data-driven attacks• Strategy: Help programmers get it right “every time” with tool supportInput validation#14• Previous work has studied best-effort bugfinding• Useful, but misses many bugs• Challenge: verifying absence of (certain kinds of) bugs• Verification has many benefits• For developers: (1) prevents shipping insecure code; (2) integration into build & QA process fixes bugs early (like regression testing)• For users: provides a security metric• Also, in our experience, verification finds more bugsWhy focus on verification?#15• Experiment: Can CQual verify absence of u/k bugs?• Sound whole-kernel analysisRefresher: user/kernel security holes• Found 10 exploitable holes in Linux 2.4.23 core• Sparse: missed all 10 bugs; 7000 annotations; many FPs• MECA: missed 6/8 bugs; 75 annotations; very few FPs• Lesson: Soundness matters!• Cost: 90 min. CPU time, 10GB RAM on 800MHz Itanium• Conclusion: Memory usage is a key challenge for scalability300K LoCSize287Annotations10Bugs532.4.23-defaultWarningsLinux kernel#16• Reduce space complexity of CQual’s CFL reachability analysis, by generating summaries for each module:for (f in source-files) read f; minimize CFL graph by rewrite rules; store graphread all graphs, & link together; perform CFL reachabilityNew: Modular type inferenceu v w u wu v w( )rewrites tooru v w u wu v w)rewrites tooru v w u wu v w( (rewrites toor() )u v w u v w[v ineligible for deletionor) )(If v has local scope, rewrite & delete v (unless ineligible — see below)#17• Experiment: Can CQual verify absence of fmt str bugs?• Sound whole-program analysis• Early indications: 1) polymorphic type inf + partial field sensitivity help enormously; 2) FPs are very rare.Preliminary experiments: Format string holes83k / 163k33k / 136k26k / 221k21k / 73k2k / 34k24k / 126k3k / 103kLOC.c / .i0/0/none 0/0/none(4 others)0/0/yes (×2) 0/0/noneapache0/0/yes(×12) 0/0/nonesshd0/0/yes(×2)