Here is an incomplete list of projects that we have worked on throughout the years. Our bitbucket and github pages houses various projects in progress as well as the source for this site. Check there for new and nascent software.
Timing analysis of TCP servers for surviving denial-of-service attacks.
Denial-of-service attacks are becoming more frequent and sophisticated. Researchers have proposed a variety of defenses but can we validate a server implementation in a systematic manner? Atasyn focuses on a particular attack, SYN flooding, where an attacker sends many TCP-connection requests to a victim's machine. It automatically transforms a TCP-server implementation into a timed automaton, and it transforms an attacker model, given by the output of a packet generator, into another timed automaton.
Scalable sensor network simulation with precise timing.
Avrora is a set of simulation and analysis tools for programs written for the AVR microcontroller produced by Atmel and the Mica2 sensor nodes. Avrora contains a flexible framework for simulating and analyzing assembly programs, providing a clean Java API and infrastructure for experimentation, profiling, and analysis.
A frontend for The Java Compiler Compiler.
JTB is a syntax tree builder to be used with the Java Compiler Compiler (JavaCC) parser generator. It takes a plain JavaCC grammar file as input and automatically generates a set of syntax tree classes, visitor interfaces, and a Java CC grammar.
We are on the cusp of a major opportunity: software tools that take advantage of Big Code. Specifically, Big Code will enable novel tools in areas such as security enhancers, bug finders, and code synthesizers. What do researchers need from Big Code to make progress on their tools? Our answer is an infrastructure that consists of 100,000 executable Java programs together with a set of working tools and an environment for building new tools. This Normalized Java Resource (NJR) will lower the barrier to implementation of new tools, speed up research, and ultimately help advance research frontiers. Researchers get significant advantages from using NJR. They can write scripts that base their new tool on NJR's already-working tools, and they can search NJR for programs with desired characteristics. They will receive the search result as a container that they can run either locally or on a cloud service. Additionally, they benefit from NJR's normalized representation of each Java program, which enables scalable running of tools on the entire collection. Finally, they will find that NJR's collection of programs is diverse because of our efforts to run clone detection and near-duplicate removal. In this paper we describe our vision for NJR and our current prototype.
A framework for end-to-end evaluation of register allocators.
RALF is a framework for end-to-end evaluation of register allocators. Built on top of gcc, RALF enables evaluation and comparison of register allocators in the setting of an industrial-strength compiler. RALF supports modular plug-and-play of register allocators without modifying the compiler implementation at all. RALF provides any plugged-in register allocator with an intermediate program representation that is independent of the data structures of the framework. In return, the register allocator provides RALF with a set of register allocation directives.
A new model for register allocation.
This project consists in developing a new model for register allocation that has fast compilation time, produces code of good quality, is able to address the many irregularities found in common computer architectures and is intuitive enough to be easily understood. We have shown that register allocation can be viewed as solving a collection of puzzles. We model the register file as a puzzle board and the program variables as puzzle pieces; pre-coloring and register aliasing fit in naturally.
The need for concurrent programming is growing, especially after the multi-core revolution. This project aims to help concurrent programmers be more productive and produce software of higher quality. This will be of paramount importance for society's software infrastructure. The project will develop general techniques that are easily applicable to many mainstream programming languages such as C++, Java, and Scala. The project's novelties are a notion of specified orders along with a program logic and machine-checked proofs of well-known concurrent algorithms. The project's impacts are approaches to concurrent programming that allow programmers to write once, prove once, and run efficiently anywhere. The investigator will work with a PhD student on the project and will teach the results to students in an undergraduate course and a graduate course.
For concurrent programs, programmers often face a mismatch between their assumptions about execution and the memory model of a specific architecture. For example, a programmer may need two instructions to execute in order for the program to be correct, yet most architectures execute out of order. This project will enable programmers to specify such assumptions, prove correctness, and run efficiently on a wide variety of architectures. Specified orders are easier to understand, reason with, and optimize than existing mechanisms such as barriers (assembly language), atomic orderings (C++), and volatiles (Java, Scala).
On the Correctness of Transactional Memory Algorithms
Transactional Memory (TM) provides programmers with a high-level and composable concurrency control abstraction. The correct execution of client programs using TM is directly dependent on the correctness of the TM algorithms. In return for the simpler programming model, designing a correct TM algorithm is an art. We have introduced a language for architecture-independent specification of synchronization algorithms that assists in the design of correct TM algorithms along with a new correctness condition, markability, and a sound program logic called synchronization object logic (SOL) that supports reasoning about the execution order and linearization orders of method calls.
Object-oriented languages such as C++, C#, and Java have brought us software libraries that are large, well tested, and easy to re-use. However, we have reached a point where many applications are dwarfed by the libraries they import. As programmers continue to develop layers of useful libraries, programmers can work at higher and higher levels of abstraction. The trade-off for a programmer is straightforward: if 10 lines of code that rely on massive, well-tested libraries can do the same as 100 lines of code, most programmers will write the 10 lines of code. As the size and power of libraries increase, the security and efficiency of application software decrease. The problem is that the massive libraries usually add complexity and bloat to even simple tasks. Thus, we pay for the high programmer productivity with software that has a large attack surface and inefficient execution. The overarching goal of the proposed project is to exploit synergy of static and dynamic program analysis techniques to tackle the security and inefficiency problems in modern software systems.
Type-correctness by type-checking
This work brings the benefits of static typechecking to self-interpreters, self-applicable partial evaluators, and other kinds of self-applicable metaprograms. A key result is that type-correctness properties -- that a self-interpreter preserves the type of the input program, that a program transformation changes the type in the expected way, etc -- are guaranteed simply by type-checking.
Objects on the head of a pin.
Virgil is a light-weight object-oriented programming language that is designed for building software for resource-constrained embedded systems at the lowest level. Microcontroller programmers can now develop complete software systems, including hardware drivers and OS services, in one language, without the need to resort to unsafe libraries or native code. Virgil also provides a whole-program compiler system that applies novel global optimization techniques to produce efficient machine code that runs directly on the hardware, without the need of a virtual machine or a language runtime system.