TrustInSoft joins HexaTrust

Hexa_Logocircle

TrustInSoft now joins HexaTrust . The HexaTrust club was founded by a group of French SMEs that are complementary players with expertise in information security systems, cybersecurity and digital trust.

TrustInSoft unique value proposal is the ability to provide guarantees on safety and security of the software. Joining HexaTrust now leverages this value proposal in a more integrated offer, reaches more customers.

PolarSSL Verification Kit

polarssl_logo

An SSL Stack free of flaws

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

No More Heartbleed

heartbleed

The Heartbleed Bug (http://heartbleed.com/) is a severe vulnerability in OpenSSL a popular cryptographic software library. This weakness allows stealing the information protected, by the SSL/TLS encryption used to secure the Internet.

OK. So one more bug has been found. What’s next? Maybe a second Heartbleed? To address this issue, at TrustInSoft, we rely on mathematical methods to provide guarantees on existing software. For instance, we created the PolarSSL Verification Kit. PolarSSL is an alternative to OpenSSL. The PolarSSL Verification Kit guarantees the immunity to the following weaknesses: CWE 119 to 127, 369, 415, 416, 457, 476, 562, 690. The Verification Kit tells you how to compile, configure, and use PolarSSL to benefit from these guarantees. It means that a flaw similar to Heartbleed cannot occur if you follow the verification kit.

All the bugs we found (for instance CVE-2013-5914) have been reported to Paul Bakker, main designer and maintainer of PolarSSL.

Now, if you want, you will not suffer from the next heartbleed. Buy TrustInSoft’s PolarSSL Verification Kit: being on the safe side is cheaper than you imagine.


contact@trust-in-soft.com

NIST assessment

samate How is it possible to protect smart phones, information systems and computers from cyber threats? To answer these questions NIST launched the SATE exhibit. TrustInSoft technology was the only one to meet SATE V Ockham Sound Analysis Criteria. full story

TrustInSoft technology meets NIST high assurance standards

Press release

lets_build

How is it possible to protect smartphones, information systems, and computers from cyber threats? How is it possible to develop high-quality software able to resist common cyber threats?

To answer these questions, the National Institute of Standards and Technology (NIST) launched the Static Analysis Tool Exposition (SATE). This exposition is designed to compare static analysis tools that find security-relevant defects in source code. This year, for the first time, the NIST introduced the SATE V Ockham Sound Analysis Criteria.

How is it possible to develop high-quality software able to resist common cyber threats?

These criteria are meant to rule out tools that report even a single incorrect finding. TrustInSoft technology was the only one to attempt to meet Ockham criteria requirements running on the Juliet 1.2 test suite from NIST. Moreover, TrustInSoft technology succeeded in satisfying the Ockham criteria for all five of NIST’s classes of weaknesses.

Technology behind the success

In the last 10 years, TrustInSof Technology was designed by CEA LIST and INRIA using funding from aeronautics and nuclear industries. The technology allows for comprehensive mathematical security guarantees on real software implementations.

Now, TrustInSoft brings the reliability of critical systems software to the IT industry.

TrustInSoft technology is able to achieve this level of quality because it relies on advanced collaboration mechanisms between formal methods. Collaboration between these state-of-the-art algorithms creates a new dimension in formal methods.

Now, TrustInSoft brings the reliability of critical systems software to the IT industry. For instance, several open-source modules have been validated thanks to TrustInSoft technology and are now immune to common cyber threats.

So, what will change?

Collaborative formal methods are now able to ensure the immunity of widely used pieces of software against the most common threats. This means that any organization in charge of designing or integrating software must deploy such state-of-the-art static analysis methods. This habit will significantly reduce the impact of cyber threats.

See also: No more heartbleed.

See also: PolarSSL verification kit.

For any information on products or services, please contact us

Cybersecurity 2020

What will be the future of software design?

Download PDF

Back in 2011, you just had to open a malicious PDF file and someone could take complete control of your smartphone.

How will cybersecurity impact software design in the year 2020? To answer this question, let’s consider an example from the past. In 2011, iOS 4.3.3 was running on iPhone devices. All you had to do was open a malicious PDF file and someone could take complete control of your phone: potentially spying on you, sending messages, or tracking your location. Today, we hope that this is no longer the case.

But why must we merely hope? Why is there no guarantee of the quality and safety of our software?

Experts will explain that this is because software is complicated. It is intricate to design and costly to validate—and this is not getting any better. After all, trends from the past 10 years demonstrate that the size of software is increasing exponentially. TrustInSoft brings high-quality software methods and tools from mission-critical systems to the IT world.

At TrustInSoft, we believe that the time has come to revolutionize software validation. TrustInSoft’s founders have created tools and methods used for mission-critical systems such as energy and aeronautics. Now, TrustInSoft is bringing these high-quality software methods and tools to the IT world.

We provide mathematical guarantees ensuring that software is immune to the most common security flaws. Applicative and system-level software will be immune to attacks used today by hackers.

For instance, TrustInSoft has completely secured an open-source implementation of an SSL/TLS communication stack (the protocol used in HTTPS). We are able to guarantee that if you use the stack in the proper manner, it is immune to the most common flaws (including buffer overflows and any other memory errors).

So, what will change from now on? Now, you have the technological power to ensure immunity against all common security flaws. Now, you have the power to make it exceedingly difficult for hackers to penetrate your systems.

But will this increased cybersecurity make antivirus software obsolete? We suspect not, because phishing attacks and other “wrong manipulations” (such as the installation of bad executable programs) will continue to occur.

In 2020, then, antivirus software will intelligently monitor behaviors to prevent “wrong manipulation” from damaging your system. At the same time, both applicative and system-level software will be immune to attacks used today by hackers—thanks to TrustInSoft.

See also: Polar SSL Verification Kit.

Welcome Julien!

julien's photo
TrustInSoft is proud to welcome Julien Cretin as Research Engineer. Julien has just defended his PhD thesis on type systems a few days ago.

Julien’s rigorous approach and expertise of the Coq proof assistant will fit right in at TrustInSoft!