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 TrustInSoft will 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.
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.