Visible to the public Combining Property-based Testing and Fuzzing

Property-based random testing, popularized by QuickCheck [2], is a form of random testing in which the developer writes properties about input/output pairs that the system under test (SUT) should satisfy. Properties can be fairly sophisticated.


Visible to the public TWC: Medium: Collaborative: Flexible and Practical Information Flow Assurance for Mobile Apps

This project is developing tools and techniques for cost-effective evaluation of the trustworthiness of mobile applications (apps). The work focuses on enterprise scenarios, in which personnel at a business or government agency use mission-related apps and access enterprise networks.


Visible to the public A Formal Specification of x86 Memory Management


We are developing a formal and executable x86 ISA specification that includes memory management via paging and segmentation. We regularly use this specification to mechanically verify user-level x86 machine-code programs. Our recent efforts have been devoted to developing a theory for reasoning about system-level programs that are aware of memory management mechanisms like paging.