TrustInSoft is among the 10 most innovative companies in 2015

Thanks to its unique ability to deliver guarantees on software, TrustInSoft has been selected among the 10 most innovative companies in 2015.

Here is our pitch.

Associated slides:

Here are the highlights of RSA Conference Innovation Sandbox 2015

Thank you for all the constructive interactions at our kiosk after the pitch session.

Read the Full press release.

TrustInSoft is ready to secure connected cars!


TrustInSoft has been selected among 8 french companies to tackle the US market for connected vehicules.
The jury was composed of selected experts:

  • Dr. Chris Urmson, Director, Self-Driving Cars Project Google,
  • Dr. Peter Sweatman, Director, University of Michigan Transportation Research Institute UMTRI, University of Michigan,
  • Dr. Andrew Brown, Vice President and Chief Technologist, Delphi
  • Mr. Phil Abram, Chief Infotainment Officer, General Motors Corporation,
  • Mr. Thomas West, California Program for Advanced Transportation Technology (PATH), The University of California à Berkeley

Here is what TrustInSoft is bringing to the table.

1) TrustInSoft is a software security startup that has already made great strides in verifying communication stacks, or the vulnerable interaction between a connected “Thing” and the internet.

For example, TrustInSoft’s static source code analysis tool has been instrumental in finding and eliminating flaws in smart factories, where computers communicate wirelessly with the factories’ assembly machines. By securing the wireless communication stack between the internet and these machines, cars are no longer vulnerable to hackers’ attempted exploitation.

2) Thanks to a growing awareness of security issues plaguing wireless components—including routers—it soon won’t be a cost-effective business model for assembly companies to ignore the security of software components. Once end-users start to demand higher security from every level, router-branding companies, for examples, won’t be able to afford to sell components with anything less than flawless software.

TrustInSoft is able to comprehensively guarantee the absence of entire families of software flaws through the application of multiple formal models. Soon, as awareness grows, companies who can claim “TrustInSoft Verified” status for their connected vehicules’ software components will gain more customers and more profits, despite the cost of thorough source code verification.

TrustInSoft in the Top 10 Finalists of the “Most Innovative Company” contest


PDF Version


TrustInSoft Recognized For Eradicating Software Security Flaws

BEDFORD, MA – MARCH 24, 2015 – TrustInSoft today has been named one of 10 finalists for RSA® Conference Innovation Sandbox Contest 2015, which is celebrating its 10-year anniversary this year. On Monday, April 20, 2015, TrustInSoft will have the opportunity to showcase its innovative information security technology to the Innovation Sandbox Contest panel of judges for a chance to be named “Most Innovative Company at RSA Conference 2015.”

Innovation Sandbox Contest promotes new approaches to information security technology, provides advice and counsel for entrepreneurs, and exposes the RSA Conference community to venture capitalists, industry experts, senior level business practitioners and thought leaders.

“Success awaits those that are named to the top 10 finalists for RSA Conference Innovation Sandbox Contest,” said Sandra Toms, vice president and curator for RSA Conferences. “Year after year, finalists have gained visibility and validation within the information security industry that has catapulted them to new heights. Many past winners and finalists have experienced high growth and increased funding, and we expect the same with this year’s top 10.”

Currently, companies try to increase their cyber protection by adding more and more layers of security onto their software. Since none of these layers is guaranteed secure, though, hackers are still able to exploit vulnerabilities in even the smallest software flaws.

TrustInSoft is putting an end to this game of cat-and-mouse by changing the way software security works: by providing tools and services able to mathematically guarantee that software is immune to entire families of known flaws. Now, TrustInSoft’s customers—spanning industries including aeronautics, space, defense, energy, telecommunication, Internet of Things, and IT—are able to deploy their software with an unparalleled level of confidence and trust. TrustInSoft can guarantee immunity against even the most insidious known flaws: for example, buffer overflows indicating Heartbleed-like attacks, or hidden flaws known as zero-days. No other company is able to provide this level of trust in existing software.

“As a finalist for the 2015 Innovation Sandbox Contest, we have the unique opportunity to demonstrate to a worldwide audience how our innovative source code analyzer not only reduces cyber-threats, but also cuts validation and verification costs,” said TrustInSoft CEO Fabrice Derepas. “This incredible opportunity should really help to catapult our US growth.”

The “Most Innovative Company at RSA Conference 2015” winner will be determined at the conclusion of Innovation Sandbox Contest, after each finalist gives a short presentation to a panel of judges that includes Asheem Chandna, partner at Greylock Partners; Gerhard Eschelbeck, vice president of security engineering at Google; Renee Guttman, vice president for information risk at Accuvant; Patrick Heim, head of trust and security at DropBox; and Paul Kocher, president of Cryptography Research.

Additional information about the “Most Innovative Company at RSA Conference 2015” and Innovation Sandbox Contest can be found at:

About TrustInSoft

TrustInSoft is a French startup company located in Paris, incorporated in 2013.

TrustInSoft produces TrustInSoft Analyzer, an advanced static source code analyzer, based on the open source Frama-C platform. TrustInSoft Analyzer enables software developers and integrators to exhaustively detect the most frequent and dangerous families of threats before deployment: this unique feature has been recognized by NIST, officially setting TrustInSoft apart from other software analysis companies. TrustInSoft also offers professional services and expertise to formally audit safety and security-critical existing software components.
For more information visit

About RSA Conference

RSA® Conference is the premiere series of global events where the world talks security and leadership gathers, advances and emerges. Whether attending in the U.S., the EMEA region, or the Asia-Pacific region, RSA Conference events are where the security industry converges to discuss current and future concerns and get access to the people, content and ideas that help enable individuals and companies to win, grow and do their best. It is the ultimate marketplace for the latest technologies and hands-on educational opportunities that help industry professionals discover how to make their companies more secure while showcasing the most enterprising, influential and thought-provoking thinkers and leaders in security today. For information on events, online programming and the most up-to-date news pertaining to the information security industry visit

Media Contacts:
Fabrice Derepas
+33 970 44 75 87

Kim Diesel
+1 512-872-7516

Read the full press release from RSA Conference web site.

Join us in San Francisco on April 20th, Moscone Center North, Room 134 from 1:00PM to 5:30PM.


2015 Internships at TrustInSoft

TrustInSoft is a 1.5 year old startup that changes the rules in cybersecurity. TrustInSoft is the software publisher of the software analysis Frama-C platform.
Our only motto is simple: make the formal methods accessible to the majority of software developers.
If you feel up to the challenge, send a resume and a motivation letter to

jobs [at]

and explain why you are the right person for one or more of the following subjects.
If you are thinking of other interesting subjects, do not hesitate to submit a short description, we will tell you if we can match these with our needs.


Subject #1: Implement new formal analyses of C programs

Beyond the absence of buffer overflows and of other undefined behaviors harmful to security, some higher-level properties can be verified at the level of C implementations. For instance, the execution time of cryptographic functions must be independent of the secrets being handled. Experimental options in Frama-C allow to verify that the secrets do not influence the execution path or the addresses dereferenced by the program ( An objective will be to improve these prototypes.
Other properties worth verifying can be taken from CWE-658. This includes the analysis of security measures that would be broken by an optimizing compiler (CWE-14) and “Time Of Check Time Of Use” (TOCTOU) conditions. Another objective will be to implement TrustInSoft plug-ins for these properties. The candidate needs to have a strong understanding of abstract interpretation and dataflow analysis techniques. The development will be in OCaml and a strong proficiency in OCaml is necessary.

Level: Master 2

Subject #2: Formal verification of properties of libotr

The libotr library ensures the confidentiality, integrity and authenticity of the personal messages sent through several chat applications, such as Pidgin. Programming errors in this C library could completely annihilate the benefits of cryptography by allowing an ill-intentioned third party to access the data before encryption or after decryption, or even to execute arbitrary code.

This internship will consist in applying the static analyzer TrustInSoft Analyzer, based on Frama-C, to verify the absence of well-known families of security vulnerabilities (including buffer overflows) in the libotr library.
This internship requires familiarity with the C language. A first experience with Frama-C or with the difficulties intrinsic to the implementation of safe cryptographic functions would be a plus.

Level: Master 2

Subject #3: Deploy and adapt an automatic testing framework for the new Web GUI of TrustInSoft Analyzer.

This tests will be implemented with the Selenium tool under Linux using the most appropriate language among Java, Javascript or OCaml.

Level: 2nd/3rd year Engineer degree

Prove & Run and TrustInSoft join forces to increase software security

pdf version


Software is getting increasingly entwined with our daily lives, whether through our mobile devices (smartphones, tablets, laptops), Cloud services, or the Internet of Things. At the same time, industrial applications that used to be independent are increasingly connected to other systems. Our increasing reliance on software, whether in industrial or personal settings, is paralleled by an increasing exposure to security issues that can have severe consequences.

Together, Prove & Run and TrustInSoft aim to raise the quality and security of software development projects to the very high levels required in today’s markets while taking into account real-world constraints such as time-to-market, cost and required skill levels. To this avail, Prove & Run and TrustInSoftwill market a shared offering, including tools and services, to address the security needs of complete software stacks, from the most sensitive and exposed low level components that support the security of the whole device (microkernels, hypervisors, bootloaders) to the higher-level functions (applications and libraries), with adequate solutions for both new and existing components.

Prove & Run and TrustInSoft have strong roots in the academic community and are focused on industrializing technical approaches developed over decades of research in the field of formal methods by INRIA, the CEA and public universities. This new offering combines the strengths of both technical approaches in order to better serve our customers” said Dominique Bolignano, Prove & Run’s CEO.

Prove & Run and TrustInSoft share a common approach to software security. This approach is based on ground-breaking technologies to help their customers deliver perfect zero-default products. The partnership between the two companies enables us to assess the security of a complete software system, ranging from low-level to high-level software containing open source, legacy and custom elements” said Fabrice Derepas, TrustInSoft’s CEO.

About Prove & Run

Prove & Run produces the ProvenTools, a complete software development toolchain that enables a software engineer to build formal models of software components and then gradually refine these models into implementation-level models, while maintaining perfect coherence between each level. This approach allows to get as close as possible to zero-bug software. The ProvenTools are forged to deal with the most sensitive software components (OS kernels, hypervisors, lifecycle managers, secure bootloaders, etc.) and to meet the highest security requirements (CC EAL7 and beyond). Prove & Run licenses the ProvenTools as well as off-the-shelf software components built with them. This offering is complemented by a comprehensive set of consulting services to help its customers to create highly secure software components.

About TrustInSoft

TrustInSoft produces the TrustInSoft Analyzer, an advanced static source code analyzer, based on the open source Frama-C platform. The TrustInSoft Analyzer enables software developers and integrators to exhaustively detect the most frequent and dangerous families of threats: this unique feature has been recognized by NIST and guarantees that TrustInSoft customers’ products do not contain hidden technical zero-days. TrustInSoft offers professional services and expertise to audit safety- and security-critical existing software components without disrupting their existing development processes. TrustInSoft licenses the TrustInSoft Analyzer and sells source code formal verification services. TrustInSoft also licenses ready-made formal verification reports for major Open Source components: these reports bring guarantees about the security and reliability of the software stacks and are instantly useful to all software engineers relying on these components. The first available report guarantees that the PolarSSL stack is immune to all forthcoming Heartbleed-like zero-days.

For more information, please contact TrustInSoft ( and Prove & Run (

© Prove & Run S.A.S. & TrustInSoft S.A.

pdf version

Fast & Serious


TrustInSoft won the “Grand Prize” during the 6WIND “Speed Matters” contest. So we got the nice 50mph green car on the picture! We already knew the power of 6WIND software, that can unleash the speed of multicore processors to create incredibly fast telecom equipment with standard hardware.

Now, thanks to TrustInSoft, there is a mathematical assessment of 6WIND software’s tremendous reliability. At TrustInSoft, we have verified that the DPDK component at the core of the software is immune against any cyber-attacks related to memory errors.

Network Function Virtualization (NFV) represents a major shift in the telecommunication and networking industry. Software plays a growing role in making telecom equipment efficient and easy to operate. Ensuring the safety and the security of the software layers, such as 6WIND’s DPDK, that make this revolution possible is a major milestone in having communication services with a guaranteed reliability.

Software-Defined Networking and Security

Software-Defined Networking (SDN) is a new approach to building networks; previously hardwired network topology gets replaced with a software implementation. For large-scale networks (think “cloud”), the additional flexibility and efficiency make all the difference in the world.

Within Software-Defined Networking, one trend is to move data using off-the-shelf, generalist server processors rather than specialized integrated circuits (ASIC). Again, to much flexibility and efficiency even within the spectrum of SDN solutions.

The security-sensitive, however, may be concerned with the loss of the security that was implicit in the relative inefficiency of the old ways. When the only way to adjust the routing requires physical access to a room of switches, security is “enhanced” as a consequence of this very limitation.
The new programmable ASICs for Software-Defined Networking may be susceptible to attacks that previous, dumb ASICs were impervious to by virtue of being dumb. And of course, generalist processors can run arbitrary code, expanding the possibilities for unintentional failure and malicious appropriation.

How do you make sure that the software works in Software-Defined Networks?

TrustInSoft verified safety properties for part of an Open-Source software component found in many SDN switches, the DPDK framework from The Git repository reveals that the main contributors are leading SDN companies such as Intel or 6WIND. The perimeter of the study was the testpmd application, plus the parts of the DPDK library exerted by testpmd. The verified properties were the absence of undefined behaviors, including all the memory errors and integer overflows that are at the root of many bugs and security vulnerabilities.

The few defects found were minor in the extreme, and still the code-changes to fix them were well-received by the DPDK community. Interestingly, with the help of TrustInSoft Analyzer to make sense of this very specialized code, Julien was also able to identify a minor optimization opportunity in this code already written with an eye towards performance. But the important fact is that since the study, carried out to completion, did not identify any Heartbleed-like memory error, no such errors exist in testpmd.

So, then, how do you make sure that SDN software works and is secure? We think that one natural step is to extend the analysis initiated by Julien to the rest of DPDK, and then to the other software components of an SDN device, using TrustInSoft Analyzer. Not to mention other software layers that are critical to the network’s security.

No More Heartbleed


The Heartbleed Bug ( 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.

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