CyLab faculty earn Amazon Research Awards

CyLab’s Limin Jia, Bryan Parno and Corina Pasareanu recently received Amazon Research Awards in the category of automated reasoning.

Proposals were reviewed for the quality of their scientific content and their potential to impact both the research community and society. The awards will provide researchers with unrestricted funds and Amazon Web Services (AWS) promotional credits, which can be used for artificial intelligence and machine learning services. Additionally, the recipients will gain access to more than 300 Amazon public datasets and have the opportunity to participate in company events and training sessions. 

Selected CyLab projects are listed below:

Enabling one-line Rust verification with program synthesis

Limin Jia - Research Professor, Electrical and Computer Engineering (ECE)
Corina Pasareanu - Principal Systems Scientist, CyLab Security and Privacy Institute

Rust is emerging as a promising language for systems programming thanks to its good runtime performance and compiler’s support for ensuring desirable properties such as memory safety and data-race freedom. However, additional verification is needed to check functional properties and ensure software behaves as intended. This Amazon Research Award will support research projects on further lowering developers’ burden of providing annotations when using the Kani Rust verifier. More concretely, Jia, Pasareanu, and their team will look to leverage Rust type and trait invariants to generate modular test harnesses with assertions, develop a synthesis algorithm to automatically infer constraints of user-defined types guided by counterexamples during verification, and create proof harnesses for automatically checking API sequences for undesired behavior. Jia, Pasareanu, and their team will evaluate these techniques on open-source Rust crates.

“Our techniques will help lower the barrier of entry for formal verification of Rust by automatically generating program invariants and test harnesses whenever it is possible, so developers can verify properties of code with few lines of annotation,” says Jia.

“Receiving the Amazon Research Award will provide us with the funding and tools needed to facilitate the application of model checking techniques (Kani) to Rust programs, leading to the development of more reliable programs at Amazon and in the larger Rust community,” says Pasareanu.
 

Verus: Developing provably correct and reliable Rust code

Bryan Parno - Associate Professor, Computer Science and Electrical and Computer Engineering departments

Writing high-performance, low-level code that is correct, reliable and secure is notoriously difficult yet increasingly critical. With resources afforded by Amazon’s Research Award, Parno and his team are helping to develop a new tool, Verus, leveraging the sophisticated design and engineering of the Rust programming language to enable complete verification of systems code.  For example, Rust’s linearity and type checkers can greatly simplify low-level code correctness proofs.  They can even allow developers to ergonomically use sophisticated tools like separation logic to reason about shared-memory concurrency. Building on their prior systems verification research, Parno and his group will look to include dedicated automation to address verification problems that arise in systems settings.

“Thanks to Amazon’s Research Award, our group will have the opportunity to help develop the Verus language and verification tools, and demonstrate their capabilities,” says Parno. “We’ll also be able to continue our work on integrating verification into the Rust ecosystem, making these tools accessible and appealing to the Rust community.”