How can essential operators be better prepared to face upcoming cybersecurity challenges?

How can essential operators be better prepared to face upcoming cybersecurity challenges, whether they are located within the EU or elsewhere in the world?

The European Commission and the High Representative have proposed concrete measures to ensure safety and security of essential operators, betting on cooperation across member states and across EU structures.

These concrete measures can be found in this cybersecurity factsheet that shows how European citizens and businesses rely on digital services & technologies. It also highlights the rise of cyber incidents and attacks, but also underlines that awareness and knowledge of cybersecurity issues is still insufficient. The factsheet sums-up The Commission and High Representative’s different proposals to reinforce the EU’s resilience to cyber-attacks.

European Commission President, Jean-Claude Juncker could not have said it better “Cyber-attacks can be more dangerous to the stability of democracies than guns and tanks (…) Cyber-attacks know no borders and no one is immune.”

80% of European companies have experienced at least one cybersecurity incident last year (2015), according to PwC 2016 global state of information security survey. This is the biggest increase in Cyber-attacks in a decade.

In a context where attackers have unprecedented opportunities, means and scale of operations, exposed software must be hardened using the strongest techniques. TrustInSoft uses formal methods to ensure the total absence of vulnerabilities in legacy software, developed in simpler times and used in the infrastructures of essential operators.

Raphaël Rieu-Helft presented his paper at Oxford University

Our employee Raphaël Rieu-Helft attended the 9thInternational Joint Conference on Automated Reasoning, within the Federated Logic Conference at the prestigious Oxford University.

There, he presented “A Why3 framework for reflection proofs and its application to GMP’s algorithms” co-authored with Guillaume Melquiond from Inria. This framework makes it easier to write dedicated decision procedures that make full use of Why3’s imperative features and are formally verified. Raphaël uses it to formally verify GMP’s algorithms.

Have a look at his presentation here

As we are always striving for continuous scientific improvements, we are truly proud of Raphaël’s achievement.

CONGRATULATIONS Raphaël!

Applying formal methods to existing software: what can you expect?

Our CTO Benjamin Monate giving a talk at the Sound Static Analysis for Security Workshop 2018 at the National Institute for Standards & Technology (NIST).

Applying formal methods to existing software: what can you expect?

Find the slides of Benjamin’s talk at the NIST here 

Formal methods-based source code verification tools have a very strong promise: mathematically prove that a piece of software is perfect. In some specific economic sectors, new languages have been adopted to help developers build perfect-by-construction software. But the vast majority of software is not perfect-by-construction and experience shows that it comes with tons of bugs. In this talk, Monate discussed what developers can expect from the application of formal methods-based tools to existing imperfect-by-construction code bases, what they should not expect, and how such tools will help make the software better and better by incrementally reducing its hidden technical debt.

This work has been supported by the Core Infrastructure Initiative of the Linux foundation.

Meet us at NIST 2018

Are you a developer, manager, evaluator of security-critical projects? Are you a researcher in cybersecurity? Looking to slay dragons AND software vulnerabilities?

Then the 2018 Sound Static Analysis for Security two-day Workshop is for you! We are sponsoring the Workshop and are proud to have our CTO, Benjamin Monate as Guest-Speaker to discuss application of formal methods to flawed code-bases.

Register here, and join us at the National Institute for Standards and Technology (NIST) in Gaithersburg, MD on the 27th & 28th of June 2018.

You will get hands-on practical advices such as: the analysis of legacy code, uses in new developments, accountable for software quality. Most of all, master the art of expertly detecting your software security breaches.

Michele Alberti wins LOPSTR 2017 Best Paper Award

In October 2017, our dear employee, Michele Alberti attended the 27th International Symposium on Logic-Based Program Synthesis and Transformation in Namur in Belgium.

The LOPSTR series of conferences aims to stimulate and promote international research and collaboration on logic-based program development.

Michele presented the research work “Context Generation from Formal Specifications for C Analysis Tools”, co-authored with fellow researcher Julien Signoles from the CEA List – Software Security Laboratory. For its relevance, originality and technical quality, his work has won the LOPSTR 2017 Best Paper Award.

Read the paper here.

As a Start-Up company that values teamwork effort and Research & Innovation, we are truly proud of Michele’s achievement.

CONGRATULATIONS Michele!