UTCS graduate student Ashay Rane, in collaboration with colleagues from Microsoft Research, University of Michigan, Carnegie Mellon University and Cornell University, won a Distinguished Paper Award at the 26th Usenix Security Symposium last month for their paper "Vale: Verifying High-Performance Cryptographic Assembly Code."
The paper introduces a new programming language, Vale, that can more easily verify the accuracy of high-performance cryptographic code used in security applications. Normally, cryptographic implementations are either fast, but difficult to verify for correctness, or slow and easily verified. However, Vale is a flexible framework that allows for a high-performance assembly code that can be proven to be functionally correct.