Formal methods for security and privacy

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.

People

Learn who at CyLab is working in formal methods.

Subtopics

We have researchers working in the following subtopics of applications of security and privacy. Check out each of their research:

Related news

CyLab Ph.D. student receives honor for “highest quality” thesis

CyLab’s Aymeric Fromherz was recognized with an A.G. Milnes Award for his Ph.D. thesis work “judged to be of the highest quality and which has had, or is likely to have, significant impact in his or her field.”

CyLab names 2021 Presidential Fellows

Four high-achieving CyLab Ph.D. students pursuing security and/or privacy-related research have been awarded CyLab Presidential Fellowships.

A big step towards cybersecurity’s holy grail

The trek towards the holy grail of cybersecurity—a user-friendly computing environment where the guarantee of security is as strong as a mathematical proof—is making big strides.

CMU-Africa and CyLab aim to improve financial inclusion in emerging economies

Carnegie Mellon University (CMU) CyLab and CMU-Africa have established the CyLab-Africa initiative, which aims to improve the cybersecurity of financial systems in Africa and other emerging economies.

Elaine Shi receives inaugural CyLab Distinguished Alumni Award

Elaine Shi, a CyLab alum and professor at Cornell University who will join the faculty at CMU this Fall, has been selected to receive the inaugural CyLab Distinguished Alumni Award.

New programming language and tool ensures code will compute as intended

A team of researchers including CyLab's Bryan Parno published a study about a new tool that mathematically proves that concurrent programs will compute correctly.

Related Article Opens in new window

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.

See More Stories

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.

Explore Other Research Topics