From: Craig Chambers (chambers@cs.washington.edu)
Date: Sat Dec 14 2002 - 18:35:02 PST
Good ideas.
-- Craig
Sorin Lerner wrote:
>
> At OSDI (Operating Systems Design and Implementation) last week there was
> a session entitled "Robustness" with 3 apply-PL-techniques-to-systems
> papers. I attached the abstracts below (and links to the papers I was able
> to find)
>
> If there is enough interest, we could look at some of these papers in 590l
> or 590k sometime in the future. The technical content of these papers from
> a PL perspective may be low, but I think it's interesting for us to see
> the latest uses of PL techniques in a systems conference. It may also give
> us some insight on how to improve the acceptance of our own current/future
> work by the systems community. We can also bundle up multiple of these
> papers in one week, since they should be pretty easy to read.
>
> -------------------------------------------------------------------------
>
> Defensive Programming: Using an Annotation Toolkit to Build DoS-Resistant
> Software
>
> Xiaohu Qie, Ruoming Pang, and Larry Peterson, Princeton University
>
> Abstract
>
> This paper describes a toolkit to help improve the robustness of code
> against DoS attacks. We observe that when developing software, programmers
> primarily focus on functionality. Protecting code from attacks is often
> considered the responsibility of the OS, firewalls and intrusion detection
> systems. As a result, many DoS vulnerabilities are not discovered until
> the system is attacked and the damage is done. Instead of reacting to
> attacks after the fact, this paper argues that a better solution is to
> make software defensive by systematically injecting protection mechanisms
> into the code itself. Our toolkit provides an API that programmers use to
> annotate their code. At runtime, these annotations serve as both sensors
> and actuators: watching for resource abuse and taking the appropriate
> action should abuse be detected. This paper presents the design and
> implementation of the toolkit, as well as evaluation of its effectiveness
> with three widely-deployed network services.
>
> <could not find this paper on-line>
>
> -------------------------------------------------------------------------
>
> Using Model Checking to Debug Device Firmware
>
> Sanjeev Kumar and Kai Li, Princeton University
>
> Abstract
>
> Device firmware is a piece of concurrent software that achieves high
> performance at the cost of software complexity. They contain subtle race
> conditions that make them difficult to debug using traditional debugging
> techniques. The problem is further compounded by the lack of debugging
> support on the devices. This is a serious problem because the device
> firmware is trusted by the operating system.
>
> Model checkers are designed to systematically verify properties of
> concurrent systems. Therefore, model checking is a promising approach to
> debugging device firmware. However, model checking involves an exponential
> search. Consequently, the models have to be small to allow effective model
> checking.
>
> This paper describes the abstraction techniques used by the ESP compiler
> to extract abstract models from device firmware written in ESP. The
> abstract models are small because they discard some of the details in the
> firmware that is irrelevant to the particular property being verified. The
> programmer is required to specify the abstractions to be performed. The
> ESP compiler uses the abstraction specification to extract models
> conservatively. Therefore, every bug in the original program will be
> present in the extracted model.
>
> This paper also presents our experience with using Spin model checker to
> develop and debug VMMC firmware for the Myrinet network interfaces. An
> earlier version of the ESP compiler yielded models that were too large to
> check for system-wide properties like absence of deadlocks. The new
> version of the compiler generated abstract models that were used to
> identify several subtle bugs in the firmware. So far, we have not
> encountered any bugs that were not caught by Spin.
>
> http://www.cs.princeton.edu/~skumar/papers/osdi02.pdf
>
> -------------------------------------------------------------------------
>
> CMC: A Pragmatic Approach to Model Checking Real Code
>
> Madanlal Musuvathi, David Y.W. Park, Andy Chou, Dawson R. Engler, and
> David L. Dill, Stanford University
>
> Abstract
>
> Many system errors do not emerge unless some intricate sequence of events
> occurs. In practice, this means that most systems have errors that only
> trigger after days or weeks of execution. Model checking 4 is an effective
> way to find such subtle errors. It takes a simplified description of the
> code and exhaustively tests it on all inputs, using techniques to explore
> vast state spaces efficiently. Unfortunately, while model checking systems
> code would be wonderful, it is almost never done in practice: building
> models is just too hard. It can take significantly more time to write a
> model than it did to write the code. Furthermore, by checking an
> abstraction of the code rather than the code itself, it is easy to miss
> errors.
>
> The paper's first contribution is a new model checker, CMC, which checks C
> and C++ implementations directly, eliminating the need for a separate
> abstract description of the system behavior. This has two major
> advantages: it reduces the effort to use model checking, and it reduces
> missed errors as well as time-wasting false error reports resulting from
> inconsistencies between the abstract description and the actual
> implementation. In addition, changes in the implementation can be checked
> immediately without updating a high-level description.
>
> The paper's second contribution is demonstrating that CMC works well on
> real code by applying it to three implementations of the Ad-hoc On-demand
> Distance Vector (AODV) networking protocol 7. We found 34 distinct errors
> (roughly one bug per 328 lines of code), including a bug in the AODV
> specification itself. Given our experience building systems, it appears
> that the approach will work well in other contexts, and especially well
> for other networking protocols.
>
> http://www.stanford.edu/~engler/osdi2002.pdf
>
> _______________________________________________
> Cecil mailing list
> Cecil@cs.washington.edu
> http://mailman.cs.washington.edu/mailman/listinfo/cecil
_______________________________________________
Cecil mailing list
Cecil@cs.washington.edu
http://mailman.cs.washington.edu/mailman/listinfo/cecil
This archive was generated by hypermail 2.1.5 : Sat Dec 14 2002 - 18:29:16 PST