PolarSSL Verification Kit

Introduction

The PolarSSL library (now known as mbed TLS) is a dual-licensed (GPLv2 or proprietary) implementation of the SSL and TLS protocols, plus the respective cryptographic algorithms and support code required. Since SSL libraries play such a crucial role in internet security, TrustInSoft developed a report that mathematically proves PolarSSL is immune to the most common security flaws.

The PolarSSL Verification Kit is a report that describes how to compile, configure, and use PolarSSL in order to remain immune from CWE 119 to 127, 369, 415, 416, 457, 476, 562, 690. We used TrustInSoft Analyzer (recognized by NIST) to generate this report.

Benefits

The PolarSSL Verification Kit guarantees the quality of the PolarSSL stack source code. We describe a PolarSSL configuration and provide the artifacts necessary for PolarSSL’s formal verification. If you follow the Verification Kit’s recommendations, you can be sure that zero-day exploits similar to Heartbleed are not present in your system’s SSL stack.

Technology

Such a verification is possible because it relies on formal methods present in TrustInSoft Analyzer. This source code analyzer uses mathematical techniques to detect any flaw that might be present. For this reason, TrustInSoft Analyzer is used to validate mission-critical software in objects such as airplanes, military cryptographic systems, nuclear reactors, space probes, and trains.

To get a PolarSSL Verification Kit on another version or on mbed TLS, please contact us using the form here.