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
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 (http://blog.frama-c.com/index.php?post/2011/12/31/Do-not-use-AES-in-a-context-where-timing-attacks-are-possible). 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.
Level: 2nd/3rd year Engineer degree