June 7th marks the start of the coding phase of Google’s Summer of Code, a global program where students code for an open source organization. TrustInSoft is proud to announce that this year they will be offering free tools to students to take advantage of the power of formal methods to verify their source code is correct, safe, and secure.
You may know that open source code can be found nearly everywhere in all industries. It is a wonderful invention that facilitates the development of many new technologies each year. Its widespread use is why it is important to be certain that there are no bugs in those programs. Undefined behaviors, a specific type of bug that stems from incorrect coding, can wreak havoc on a program and the technology it is being used in. They are complex to detect and can lead to disastrous consequences.
Luckily for you Googlers, you won’t have to worry about bugs persisting in your code project this summer! TrustInSoft is offering you two free tools to use to formally verify your code.
What does formal verification mean, and what are the tools available? Read on to find out.
TrustInSoft’s AST for Googlers relies on the power of formal methods, which are a series of mathematical and logical reasonings that allow to produce a “mathematical twin” of source code. In this mathematical context, it is possible to prove the absence of source code bugs for any input.
Formal methods used to require a high level of expertise to employ, but with TrustInSoft’s tools, any software developer can unlock the power of formal methods verification thanks to its simple implementation and user-friendly graphical interface.
Use TSnippet to formally verify the absence of undefined behavior in short code snippets. This could be useful for small parts of your code that are very critical.
You can also simulate your code on a variety of platforms to test that it functions correctly no matter the processor used.
For open source code that is in a public repository on Github, you can use TrustInSoft CI to formally verify using existing tests that there are no bugs present in the code.
There are 0 false positives and 0 false negatives when you use TrustInSoft CI!
A tutorial is available on the TrustInSoft CI page on Github for further instructions on how to configure the tool.
TrustInSoft is a software publisher based in Paris and San Francisco dedicated to providing companies with trust in their software, by guaranteeing the safety and security of their source code using mathematical techniques known as formal methods.
Founded in 2013 by three former researchers of the French government’s Alternative Energies and Atomic Energy Commission, and based on their development of Frama-C, TrustInSoft today supports customers in a variety of industries, including aeronautics, telecommunications, industrial IoT and automotive.
Recognized by the NIST, Linux Foundation, and the RSA Conference, TrustInSoft has a long history of contributing to the software development community, especially with regards to open-source software. In addition to the heart of its technology, Frama-C, being open-source, it has contributed to the resolution of several code vulnerabilities present in open-source software.