Manos Kapritsos and collaborators win USENIX security paper award

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.