Linux Foundation takes steps to make open-source software safer

From ZDNet:

False Positive Free Testing: Pascal Cuoq, chief scientist and co-founder of TrustInSoft, has received a grant to build an open source TIS Interpreter. This program will be built from TIS Analyzer, a commercial software analysis tool based on Frama-C. Frama-C is a debugger that works by interpreting C programs statement by statement from beginning to end. It verifies with each statement whether the tested program can invoke undefined behavior.

Historically, TIS Analyzer and other programs that use Frama-C can produce false positives. With this new program, the goal is to develop a methodology that detects bugs without false positives. Thus, any bug that is reported will be a real bug.


Read full press release.

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.