Software today comes with few, if any, security guarantees. Traditionally, software vendors become aware of vulnerabilities after an attack occurs and then issue a patch that fixes that particular attack. Carnegie Mellon University CyLab researchers are looking to change all of that by employing mathematical techniques, commonly referred to as formal methods, to mathematically prove that a system is secure and protected against cyberattacks.
Learn who at CyLab is working in formal methods.
We have researchers working in the following subtopics of applications of security and privacy. Check out each of their research:
Provably-secure code incorporated into Linux kernel
This month, code from the provably correct and secure “EverCrypt” cryptographic library, which CyLab’s Bryan Parno and his team helped develop and release last year, was officially incorporated into the Linux kernel — the core of the Linux operating system.
Achieving provably-secure encryption Opens in new window
Earlier this week, a team consisting of researchers from CyLab released the world’s first verifiably secure industrial-strength cryptographic library—a set of code that can be used to protect data and is guaranteed to protect against the most popular classes of cyberattacks.
Building a verifiably-secure internet
In security, almost nothing is guaranteed. It's impossible to test the infinite ways a criminal hacker may penetrate a proverbial firewall. But what if, by the laws of mathematics, something could be proven to be secure without running an infinite number of test cases?
Fourteen years later, Pasareanu’s automated software-testing work awarded for retrospective impact
Fourteen years ago, CyLab associate research professor Corina Pasareanu and two of her colleagues published a paper outlining three automated techniques for checking software for bugs and vulnerabilities. This month, Pasareanu and her colleagues are receiving the 2018 Retrospective Impact Award from the International Symposium on Software Testing and Analysis (ISSTA).
Celebrating “SSL,” the unsung hero of online shopping
In the time it takes you to read this sentence, Americans are spending somewhere between $50,000 and $100,000 on retail online. In those mere seconds of time, few thought twice about sharing their credit card numbers with Amazon, or banking routing numbers with PayPal or social security numbers with their banks. We have the Secure Socket Layer (SSL) to thank for that.
CyLab's Bryan Parno shares Distinguished Paper Award win with demonstration of verifiable security
In a paper presented at the USENIX Security Symposium, Bryan Parno and a team of researchers demonstrated a new programming tool that enables high-performance cryptographic code to be verifiably correct and secure.