DANSAS 2011, Odense, August 18
|09:00 - 09:30||Coffee and breakfast rolls|
|09:30 - 09:40||Welcome|
|09:40 - 10:25||Program Analysis for Engineering Secure Web Applications (invited talk)|
|10:30 - 11:00||Fruit Break|
|11:00 - 11:25||Programming in Biomolecular Computation|
Neil D. Jones
|11:35 - 12:00||Formalizing Elections for Tractable Test Generation using Model Checking|
Joseph Kiniry and Dermot Cochran
|12:05 - 13:35||Lunch|
|14:10 - 14:35||Finding Resource-Release Omission Faults in Linux|
|14:45 - 15:10||Guarded Type Promotion|
|15:15 - 15:45||Coffee Break|
|15:45 - 16:10||Monotonicity Constraint Transition Systems and Complexity Analysis|
Amir M. Ben-Amram
|16:50 - 17:00||Announcement of best student presentation and wrap-up|
Program Analysis for Engineering Secure Web Applications (invited talk)
University of California, Davis
Web applications enable much of today's online business. Anyone with a web browser can access them, and the data they manage typically has significant value both to the users and to the service providers. Thus, they have become increasing targets of attacks. Since 2005, the most frequently reported classes of vulnerabilities have been for web applications. There are two broad classes of web application vulnerabilities: 1) application-agnostic injection flaws, and 2) application-specific access control flaws. Their detection and prevention pose an interesting challenge for program analysis. In this talk, I will present two simple, yet general characterizations of these vulnerabilities and a set of program analysis techniques to detect them.
About speaker: Zhendong Su is a Professor and Chancellor's Fellow at University of California, Davis. He received his PhD in Computer Science from University of California, Berkeley. His research focuses on developing practical techniques and tools for improving software quality and programming productivity. He serves as an Associate Editor for ACM Transactions on Software Engineering and Methodology (ACM TOSEM), co-chaired the 2009 Static Analysis Symposium (SAS), and is the program chair of the 2012 International Symposium on Software Testing and Analysis (ISSTA).
Programming in Biomolecular Computation
Neil D. Jones
University of Copenhagen
In spite of widespread discussion about connections between biology and computation, one question seems notable by its absence: Where are the programs? We take the question seriously, and propose a model of computation that is at the same time biologically plausible: the model's functioning is defined by a relatively small set of chemical-like reaction rules; programmable (by programs reminiscent of low-level computer machine code); uniform: new "hardware" is not needed to solve new problems; universal: all computable functions can be computed (in natural ways and without arcane encodings of data and algorithm); stored-program: programs are the same as data, so programs are not only executable, but are also compilable and interpretable; and (last but not least) Turing complete in a strong sense: a universal algorithm exists, able to execute any program, and not asymptotically inefficient.
The model has been designed and implemented (for now in silico on a conventional computer). This work opens new perspectives on just how computation may be specified at the biological level. One goal is to provide a top-down approach to biomolecular computation.
(joint work with Lars Hartmann and Jakob Grue Simonsen)
Formalizing Elections for Tractable Test Generation using Model Checking
Joseph Kiniry and Dermot Cochran
IT University of Copenhagen
E-voting software, particularly tallying software that computes the final outcome of elections, is notoriously under-specified and poorly tested. Elections are critical systems, and yet virtually all election systems, including those used in national and EU elections, have no formal specification. Moreover, even though the state space of non-trivial election algorithms is astronomically large, virtually all commercial and open source election system include only a handful of manual systems tests. Perhaps shockingly, counting systems are, at best, tested via the random generation of ballot boxes which are counted by multiple implementations of the tallying algorithm. Consequently, such a test method exercises a microscopically small fraction of the state space. I will summarize our research in using the Alloy model checker to formalize elections to better understand elections, discover legal irregularities, and generate a complete set of non-isomorphic ballot boxes to guarantee that every election outcome is exercised during system testing.
Refactoring is a popular technique for improving the structure of existing programs while maintaining their behavior. For statically typed programming languages such as Java, a wide variety of refactorings have been described, and tool support for performing refactorings and ensuring their correctness is widely available in modern IDEs.
(Joint work with Max Schäfer, Todd Millstein, Frank Tip, and Anders Møller)
Finding Resource-Release Omission Faults in Linux
University of Copenhagen / University of Paris 6
The management of the releasing of allocated resources is a continual problem in ensuring the robustness of systems code. Missing resource-releasing operations lead to memory leaks and deadlocks. A number of approaches have been proposed to detect such problems, but they often have a high rate of false positives, or focus only on commonly used functions. In this paper we observe that resource-releasing operations are often found in error-handling code, and that the choice of resource-releasing operation may depend on the context in which it is to be used. We propose an approach to finding resource-release omission faults that takes into account these issues. We use our approach to find over 100 faults in the drivers directory of Linux 2.6.34, with a false positive rate of only 16%, well below the 30% that has been found to be acceptable to developers.
(To be presented at the workshop Programming Languages and Operating Systems, October 2011)
Guarded Type Promotion
In Java, explicit casts are ubiquitous since they bridge the gap between compile-time and runtime type safety. Since casts potentially throw a ClassCastException, many programmers use a defensive programming style of guarded casts. In this programming style casts are protected by a preceding conditional using the instanceof operator and thus the cast type is redundantly mentioned twice. We propose a new typing rule for Java called Guarded Type Promotion aimed at eliminating the need for the explicit casts when guarded. This new typing rule is backward compatible and has been fully implemented in a Java 6 compiler. Through our extensive testing of real-life code we show that guarded casts account for approximately one fourth of all casts and that Guarded Type Promotion can eliminate the need for 95 percent of these guarded casts.
(also presented at the 2011 Workshop on Formal Techniques for Java-like Programs)
Monotonicity Constraint Transition Systems and Complexity Analysis
Amir M. Ben-Amram
University of Copenhagen / Tel Aviv Academic College
Monotonicity Constraint Transition Systems over the integers - concisely (MC,Z)-CTS - are a program abstraction where termination is decidable (an extension of the well-known Size-Change Termination). A transition system is bounded terminating when there is a function that bounds the number of transitions, in terms of the input.
We have now proved that the Bounded Termination problem for these transition-systems is also decidable (in PSPACE). Interestingly, an (MC,Z)-CTS is bounded-terminating if and only if it has a polynomial bound. Furthermore, the degree of the polynomial is also PSPACE-computable.
The significance of such bounds for a source program depends on the abstraction (the "front end"). In the most natural and obvious situation it will mean a time bound. In others, it can mean, for example, a space bound. We claim that focusing on an abstraction which is expressive while being decidable is a profitable approach to studying a program analysis question, which worked nicely for termination. It should also be applicable to Complexity Analysis.
(Joint work with Michael Vainer, Tel Aviv Academic College)