The Michigan Engineer News Center

Manos Kapritsos and collaborators win USENIX security paper award

Their paper introduces a new programming language and tool called Vale that supports flexible, automated verification of high-performance assembly code.| Short Read

A team of researchers including Prof. Manos Kapritsos has won a Distinguished Paper Award at the 2017 USENIX Security Symposium, which took place August 16–18, 2017 in Vancouver.

The paper, entitled Vale: Verifying High-Performance Cryptographic Assembly Code, introduces a new programming language and tool called Vale that supports flexible, automated verification of high-performance assembly code.

Strong cryptography is critical for security in a number of applications, from mobile computing through cloud repositories and digital currencies. Ideally, encryption should be correct, secure, and fast. However, producing verified implementations that meet these criteria is a challenge.

High-performance cryptographic code often relies on complex hand-tuned assembly language that is customized for individual hardware platforms. Such code is difficult to understand or analyze.

The Vale tool transforms annotated assembly language into an abstract syntax tree (AST), while also generating proofs about the AST that are verified via an SMT solver. Since the AST is a first-class proof term, it can be further analyzed and manipulated by proven correct code before being extracted into standard assembly. It is the hope of the researchers that Vale demonstrates that verified code can be as fast as highly-optimized, unverified code.

Prof. Manos Kapritsos received his PhD in Computer Science from the University of Texas in Austin in 2014 and joined the faculty at Michigan in 2017 after working as a postdoctoral researcher at Microsoft Research. His research interests are in the area of software systems, with a focus on fault-tolerant distributed systems. In his dissertation research, Manos reconciled replication with multithreaded execution by rethinking the 40-year-old architecture of replicated systems to enable the performance benefits of parallel execution. In post-doctoral work, he has worked to bring formal verification to distributed systems, proposing a new way of reasoning about complex distributed systems through a combination of reduction and multilevel refinement to partition them into smaller, manageable components.

Portrait of Steve Crang

Contact

Steve Crang
CSE Marketing and Communications Manager

Michigan Engineering

(734) 763-9996

3832 Beyster Bldg

Researchers
  • Manos Kapritsos

    Manos Kapritsos

    Assistant Professor, Electrical Engineering and Computer Science

BepiColombo approaching Mercury. Credit: European Space Agency

U-M researchers to help unravel Mercury, solar system mysteries

In ESA's BepiColombo mission, an examination of the particles in Mercury's upper atmosphere will shed light on what the planet is made of. | Medium Read