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.

Specifically, the code’s main use within the kernel is as part of Linux’s latest built-in Virtual Private Network (VPN). Anyone using Linux–for example, anyone using the Android operating system, which is built on a modified version of Linux–can benefit from increased confidence in the VPN service.

We’re hopeful that some of the other components within the kernel will start using our verified code as well.

Bryan Parn, Associate Professor, Electrical and Computer Engineering and Computer Science

“We’re hopeful that some of the other components within the kernel will start using our verified code as well,” said Parno, an associate professor of Electrical and Computer Engineering and Computer Science.

Parno is an integral member of a research initiative known as Project Everest, which is creating provably secure components of the HTTPS ecosystem. Last April, Project Everest released EverCrypt, the first provably secure industrial-strength cryptographic library. A cryptographic library lives at the heart of virtually every security-sensitive application.  EverCrypt provides such a library that provably protects against the most popular classes of cyberattacks.

EverCrypt is available for download on Github.