This paper presents Themis, an end-to-end static analysis tool for finding resource-usage side-channel vulnerabilities in Java applications. We introduce the notion of ε-bounded non-interference, a variant and relaxation of Goguen and Meseguer’s well-known non-interference principle. We then present Quantitative Cartesian … Read More
Kostas’s work on “Failure-Directed Program Trimming” will appear at FSE’17! Here is the abstract of the upcoming paper: We present a new program simplification technique called program trimming that aims to improve the scalability and precision of safety checking tools. … Read More
Our paper called “Component-based Synthesis of Table Consolidation and Transformation Tasks from Examples” will appear in PLDI’17! Here is the abstract: This paper presents an example-driven synthesis technique for automating a large class of data preparation tasks that arise in … Read More
Our paper on automatically detecting regular expression denial-of-service (ReDoS) vulnerabilities got accepted into TACAS’17! Static Detection of DoS Vulnerabilities in Programs that use Regular Expressions In an algorithmic complexity attack, a malicious party takes advantage of the worst-case behavior … Read More
Our work on synthesizing semantic malware signatures is accepted at NDSS’17! Here is the abstract: This paper proposes a technique for automatically learning semantic malware signatures for Android from very few samples of a malware family. The key idea … Read More
Our paper called “Component-Based Synthesis for Complex APIs” is accepted to POPL 2017 in Paris! Here is the abstract: Component-based approaches to program synthesis assemble programs from a database of existing components, such as methods provided by an API. In this … Read More
Our papers “Synthesizing Transformations on Hierarchically Structured Data” and “Cartesian Hoare Logic for Verifying k-safety Properties” have been accepted to PLDI’16!! Congratulations to Navid, Chris, and Marcelo!
Our paper called “Detecting and Exploiting Second Order Denial of Service Vulnerabilities in Web Applications” is accepted to CCS 2015 in Denver! Here is the abstract: This paper describes a new class of denial-of-service (DoS) attack, which we refer to … Read More
Our paper called “EXPLORER : Query- and Demand-Driven Exploration of Interprocedural Control Flow Properties” has been accepted to OOPSLA’15 ! Here is the abstract of the paper: This paper describes a general framework—and its implementation in a tool called EXPLORER–for … Read More
Our UTOPA group webpage is live as of September, 2015!