Main Page

From CS260r 2015
Revision as of 13:11, 15 May 2015 by Kohler (Talk | contribs) (CS 260r: Topics and Close Readings in Computer Systems)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

CS 260r: Topics and Close Readings in Computer Systems

Spring 2015—MW 1–2:30—Maxwell Dworkin 221—Eddie Kohler

Piazza signupPresenting papersUpcoming papers

CS 260r is a research seminar in computer systems. That means it’s a relatively informal course in which we learn about current research in the computer systems area, and hopefully create some research of our own. The work of the course consists of reading and presenting research papers; some homeworks; and a final project, which can be done in groups.

Each time the course is offered we have a new topic. This year the topic is building reliable systems code; we’ll try to better understand modern techniques for making systems software more robust. These techniques include, but are not limited to:

  • Ad hoc static code analyses and tools.
  • Model checkers.
  • Code verification.
  • Machine learning techniques applied to code analysis.
  • Undefined behavior detectors.
  • Testing frameworks.
  • Record-and-replay techniques.

We will read papers by many authors, but I hope we investigate several research groups’ work in depth, possibly including those of Dawson Engler, John Regehr, Andrea and Remzi Arpaci-Dusseau, Yuanyuan Zhou, Shan Lu, Luis Ceze, Jason Flinn and Peter Chen, Michael Ernst, Martin Rinard, George Candea, and Nickolai Zeldovich.

The goal of the seminar is to understand the best current research on systems software robustness. Students should also learn how to read research papers actively—that is, how to work past initial unfamiliarity with a research area toward a good understanding of its main research approaches and topics, using different kinds of reading and thinking.

The course schedule will be posted piecemeal as we go and is subject to discussion and change based on class interests.

W 1/28 Ignoring failure First, let’s read something fun:

M 2/2 Integer overflow Before you read these papers, take John Regehr’s Integer Quiz!

W 2/4 Symbolic execution

M 2/9, delayed to W 2/11 Undefined behavior, symbolic test generation

  • Questions:
    • STACK: Give examples of (1) an error that KINT would catch, but STACK would not; (2) an error that STACK would catch, but KINT would not; (3) an error that both tools would catch.
    • Optional bonus question: I believe there are at least two bugs in STACK’s Fig. 3. Can you find them?
    • UC-KLEE: What does UC-KLEE gain by initializing memory lazily? Why not just initialize memory in response to malloc() calls?

W 2/18 Reliability design patterns: Philosophy

M 2/23

    • Question: Compare and contrast the ways Minix and seL4 handle (1) IPC message formats (e.g., are variable-length messages allowed?), and (2) process hierarchies. Do the systems make similar or different choices? How do the authors justify their choices?

W 2/25

  • Question: The protection mechanisms in Nooks, like those in Minix, are designed to protect “against bugs but not against malicious code.” So do Minix and Nooks provide qualitatively equivalent protection mechanisms, or does one provide more protection than the other? If yes, mention specific potential bugs that would be handled differently by the two systems.

F 2/27

  • Thorough Static Analysis of Device Drivers, Thomas Ball, Ella Bounimova, Byron Cook, Vladimir Levin, Jakob Lichtenberg, Con McGarvey, Bohus Ondrusek, Sriram K. Rajamani, and Abdullah Ustuner, Proc. Eurosys ’06 (Anitha)
  • Question: Contrast SDV’s counterexample-guided abstraction refinement approach with KLEE’s symbolic execution engine. Give at least one similarity (of approach, of result, of type of bug that can be found, etc.) and at least two differences.

W 3/4

  • Question: Describe how Triage-style diagnosis could be combined with Pip-style failure detection, including at least one significant challenge to this combination.

M 3/9

  • Question: (1) How would you deploy PHP in the OKWS framework? What OKWS security benefits would you lose thereby? (2) Describe a security bug that Apollo could find, that would not be eliminated by the OKWS architecture.

W 3/11

  • Question: Write out a semi-formal (or formal) argument that justifies the following statement on Page 3 of Zeller: “In the best case, we have no unresolved test outcomes…[t]hen, the number of tests t is limited by t≤log2(|cx|)—basically, we obtain a binary search.”

W 3/25

  • Moving Fast with Software Verification, Cristiano Calcagno, Dino Distefano, Jeremy Dubreil, Dominik Gabi, Pieter Hooimeijer, Martino Luca, Peter O'Hearn, Irene Papakonstantinou, Jim Purbrick, and Dulma Rodriguez, Proc. NASA Formal Method Symposium (Lily)
  • Question: Write a sample function for which INFER, as in use at Facebook, would detect a bug that would not be ruled out by any Clousot-style necessary precondition. (This code doesn't need to compile—you can just make something up, and pseudocode is ok.)

M 4/6

W 4/8

M 4/13

W 4/22

Exercises

Project