Publications

• CROW: Code Diversification for WebAssembly
  Published on 2021-04-11
• Automated patch assessment for program repair at scale
  Published on 2021-04-06
• PomCho : Atool chain for choreographic design
  Published on 2021-01-20
• InSpectre: Breaking and Fixing Microarchitectural Vulnerabilities by Formal Analysis : The recent Spectre attacks have demonstrated the fundamental insecurity of current computer microarchitecture. The attacks use features like pipelining, out-of-order and speculation to extract arbitrary information about the memory contents of a process. A comprehensive formal microarchitectural model capable of representing the forms of out-of-order and speculative behavior that can meaningfully be implemented in a high performance pipelined architecture has not yet emerged. Such a model would be very useful, as it would allow the existence and non-existence of vulnerabilities, and soundness of countermeasures to be formally established. This paper presents such a model targeting single core processors. The model is intentionally very general and provides an infrastructure to define models of real CPUs. It incorporates microarchitectural features that underpin all known Spectre vulnerabilities. We use the model to elucidate the security of existing and new vulnerabilities, as well as to formally analyze the effectiveness of proposed countermeasures. Specifically, we discover three new (potential) vulnerabilities, including a new variant of Spectre v4, a vulnerability on speculative fetching, and a vulnerability on out-of-order execution, and analyze the effectiveness of existing countermeasures including constant time and serializing instructions.
  Published on 2021-01-11
• SerialDetector: Principled and Practical Exploration of Object Injection Vulnerabilities for the Web
  Published on 2021-01-07
• Friendly Fire: Cross-App Interactions in IoT Platforms
  Published on 2021-01-04
• mCoq: Mutation Analysis for Coq Verification Projects
  Published on 2020-11-24
• Trustworthy isolation of DMA devices
  Published on 2020-10-07
• Hoare-Style Logic for Unstructured Programs
  Published on 2020-09-21
• Superoptimization of WebAssembly bytecode
  Published on 2020-09-02
• Deep Generation of Coq Lemma Names Using Elaborated Terms
  Published on 2020-08-26
• Practical Machine-Checked Formalization of Change Impact Analysis
  Published on 2020-08-26
• Towards a Verified Model of the Algorand Consensus Protocol in Coq
  Published on 2020-08-26
• FixMiner : Mining relevant fix patterns for automated program repair
  Published on 2020-06-05
• An Analysis of 35+ Million Jobs of Travis CI
  Published on 2020-05-13
• Clockwork: Tracking Remote Timing Attacks
  Published on 2020-05-08
• IntRepair : Informed Repairing of Integer Overflows
  Published on 2020-04-08
• Explainable software bot contributions : Case study of automated bug fixes
  Published on 2020-03-27
• Fully Automated HTML and JavaScript Rewriting for Constructing a Self-healing Web Proxy
  Published on 2020-03-24
• A journey among Java neutral program variants
  Published on 2019-11-22