Software:TrustInSoft Analyzer

From HandWiki
Revision as of 11:37, 15 September 2023 by Importwiki (talk | contribs) (import)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
TrustInSoft Analyzer
Logo of TrustInSoft Analyzer
Developer(s)TrustInSoft company
Written inOCaml
Operating systemMicrosoft Windows, FreeBSD, OpenBSD, Linux, Mac OS X
Available inEnglish
TypeFormal verification, static code analysis
LicenseProprietary
Websitetrust-in-soft.com/product/trustinsoft-analyzer/

TrustInSoft Analyzer is a source code analyzer, analyzing code written in the C and C++ programming languages. It implements a set of various formal methods, which create mathematical proofs of the absence of undefined behavior in the analyzed code. Undefined behaviors are recognized as a major source of software vulnerabilities.[1]

Typical examples of undefined behavior, tracked by TrustInSoft analyzer, include memory management issues such as buffer overflow and uninitialized variables; arithmetic operations including division by zero and integer overflow; and race conditions. TrustInSoft Analyzer is predominantly used for software analysis in embedded systems and addresses safety and security issues within the source code. TrustInSoft Analyzer aids in establishing compliance with safety and security standards and norms[2] including ISO 26262 and MISRA C.

The analyzer is not only limited to detect undefined behavior. It can also prove that a program conforms to a formal specification of its intended functional behavior. The formal langage of specifications supported is the ANSI/ISO C Specification Language (ACSL).

Basic Example of Use

Consider the following toy example of a C code for a function computing the absolute value of its integer argument. 

int absolute_int(long x) {
   long abs_x;
   if (x < 0)
     abs_x = -x
   else
     abs_x = x;
   return abs_x;
 }

Running the analyzer will result in one alarm, positioned before statement abs_x = -x on line 4, and categorized as a "signed overflow". The alarm is accompanied with an ACSL annotation as follows. 

//@ assert -x <= 9223372036854775807

The meaning of this ACSL annotation is as follows: it gives a logical assumption that must be made in order for the code to continue execution without undefined behavior. It also implicitly mean that the analyzer was unable to guarantee that this assumption holds for any possible input x.


The user has the possibility to continue further by invoking another level of analysis, which is going to try to prove that the assertion holds, using external theorem provers. In that case, not only the proof attempt will fail, but a potential counterexample is proposed, namely the value 0x80000000 for x. Indeed, this value denotes LONG_MIN, the smallest representable integer in the C type long, which denotes the integer -9223372036854775808, making the asserted assumption false.

It is indeed a classical example of a programming mistake, computing the absolute value is not possible for LONG_MIN in C.

The ACSL language allows the users to specify a requirement on the use of their functions. On this example, the function could be preceeded by an ACSL contract as follows. 

/*@ requires x > LONG_MIN;
  @*/
int absolute_int(long x) {

The given requires clause is a precondition. It means that the function should never be called on the value LONG_MIN for x. With this extra annotation, the code can be shown free of undefined behavior. It is important to notice that the annotation above forms a contract between the function and its callers: it means that at each call to absolute_int in the rest of the program, the analyzer will attempt to prove that the precondition holds, and raise an alarm otherwise.

ACSL contracts can also contain postconditions. For example, the same function could be given a more precise contract as follows. 

/*@ requires x > LONG_MIN;
  @ ensures \result >= 0;
  @ ensures x >= 0 ==> \result == x;
  @ ensures x < 0 ==> \result == -x;
  @*/
int absolute_int(long x) {

The other annotations, introduced by the ACSL keyword ensures are post-conditions. They declare that the given formulas hold at function exit, where \result denotes the result value of the function call. These three post-conditions are indeed satisfied by the function body for any input x, and proved valid as such by TrustInSoft Analyzer.

Overview of Implemented Technologies

TrustInSoft Analyzer applies various formal methods including abstract interpretation and deductive verification via the computation of weakest preconditions. Its use of multiple formal methods results in an exhaustive analysis of the source code for undefined behavior. It follows a multi-step analysis, first using existing test suites, then an exhaustive analysis of the source code for all inputs, up to a full mathematical guarantee of the software’s compliance with a formal specification written in ACSL.

The abstract interpretation technique implemented in TrustInSoft Analyzer computes a superset of the possible values for each variable of the program at each program point, depending on the range of possible inputs.[3] This process raises an alarm whenever any undefined behavior may take place. It results in the exhaustive detection of undefined behaviors in the analyzed program. As shown by the basic example above, the alarms take the form of formulas written in the ACSL specification language. The abstract interpretation of TrustInSoft Analyzer includes a few original methods. It includes a specific analysis for detection of strict-aliasing violations.[4] To avoid a too large loss of precision when analysing code with conditional branches, it implements an original path-sensitive analysis.[5] Moreover, when the analysis is not precise enough, the user has some ways to guide of the analysis.[6]

TrustInSoft Analyzer also implements deductive verification techniques to perform formal proof. These are aimed to establish that the code under analysis conforms with specifications written in ACSL. These specifications may be written by users or, as mentioned above, generated by the tool in the form of potential alarms. In particular, this technique allows to prove that alarms raised by the abstract interpreter are false alarms. Technically, the analyzer performs some form of weakest-precondition calculus to generate proof obligations. These are mathematical formulas whose validity implies the functional correctness of the analyzed program. To verify that these formulas are valid, the analyzer calls external tools, including the Why3 generic environment for verification, and some external SMT solvers such as Alt-Ergo and Z3. Harder proofs can be performed using the Coq interactive theorem prover.

Combining various formal methods techniques, as mentioned above, has proved to be key to achieving a complete analysis of source code.[7][8]

The question of the soundness of the analyzer is addressed. The analyzer cannot be used to analyze its own code, because it is not written in C but in the OCaml language. OCaml has a great advantage for implemented methods making heavy use of symbolic representations, namely its automatic memory management.[9] Last but not least, the validity of the analyzer has been exercised through a heavy campaign of random testing,[10] using methods that were able to discover many bugs in existing C compilers.

Development and Deployment

TrustInSoft Analyzer was created in 2016, initially as a fork of Frama-C, a Framework for Modular Analysis of C programs. The three initial developers of TrustInSoft Analyzer were former developers of Frama-C. Both TrustInSoft Analyzer and Frama-C keep using the same formal specification language ANSI/ISO C Specification Language. TrustInSoft Analyzer deploys in multiple environments (e.g. Mac OS, Linux, Windows) and integrates with various tools (e.g. Google Test and Jenkins).[11] All versions of C up to 18 and C++ up to 20 are supported.[2]

TrustInSoft Analyzer is available as a standalone software under a proprietary license for customers of the TrustInSoft company. It is also available, in a restricted form, as a freely accessible web application, for experimenting and teaching.[12] Additionally, another free, fairly complete, version of the Analyzer is available on the web, able to analyze code provided the source is publicly hosted on Github.[13]


Applications and Visibility

Together with its ancestor Frama-C, TrustInSoft Analyzer has been used in several industrial-scale applications.[14] The web site of TrustInSoft maintains a list of successful industrial applications.[15] In 2016, TrustInSoft Analyzer was accredited in a NIST report to the White House Office of Science and Technology Policy, for proving the absence of CWE vulnerabilities in the PolarSSL (nowadays known as Mbed TLS) stack.[1] In 2021, TrustInSoft was selected by UBIMobility, an accelerator for autonomous vehicles technologies.[16] TrustInSoft Analyzer acquired some world-wide visibility in the press specialized in electronic and software engineering.[17][18][19]

See also

References

  1. ↑ 1.0 1.1 National Institute of Standards and Technology (2016). Dramatically Reducing Software Vulnerabilities: NiSTIR 8151. doi:10.6028/NIST.IR.8151. ISBN 978-1548477714. https://nvlpubs.nist.gov/nistpubs/ir/2016/NIST.IR.8151.pdf. 
  2. ↑ 2.0 2.1 "Source Code Security Analyzers". 23 March 2021. https://www.nist.gov/itl/ssd/software-quality-group/source-code-security-analyzers. 
  3. ↑ Canet, Géraud; Cuoq, Pascal; Monate, Benjamin (2009). "A Value Analysis for C Programs". Ninth IEEE International Working Conference on Source Code Analysis and Manipulation. doi:10.1109/SCAM.2009.22. 
  4. ↑ Cuoq, Pascal; Runarvot, Loïc; Cherepanov, Alexander (2017). "Detecting Strict Aliasing Violations in the Wild". Verification, Model Checking, and Abstract Interpretation. doi:10.1007/978-3-319-52234-0_2. 
  5. ↑ Cuoq, Pascal; Rieu-Helft, Raphaël (2017). "Result graphs for an abstract interpretation-based static analyzer". 28th French Days on Functional Languages. https://hal.science/hal-01503064. 
  6. ↑ Mattsen, Sven; Cuoq, Pascal; Schupp, Sibylle (2013). "Driving a sound static software analyzer with branch-and-bound". 13th IEEE International Working Conference on Source Code Analysis and Manipulation. IEEE Computer Society. pp. 63–68. doi:10.1109/SCAM.2013.6648185. 
  7. ↑ Cuoq, Pascal; Monate, Benjamin; Pacalet, Anne; Prevosto, Virgile (2011). "Functional Dependencies of C Functions via Weakest Preconditions". International Journal on Software Tools for Technology Transfer 13 (5): 405–417. doi:10.1007/s10009-011-0192-z. 
  8. ↑ Chebaro, Omar; Cuoq, Pascal; Kosmatov, Nikolai; Marre, Bruno; Pacalet, Anne; Williams, Nicky; Yakobowski, Boris (2014). "Behind the scenes in SANTE: a combination of static and dynamic analyses". Automation in Software Engineering 21 (1): 107–143. doi:10.1007/s10515-013-0127-x. 
  9. ↑ Cuoq, Pascal; Signoles, Julien; Baudin, Patrick; Bonichon, Richard; Canet, Géraud; Correnson, Loïc; Monate, Benjamin; Prevosto, Virgile et al. (2009). "Experience report: OCaml for an industrial-strength static analysis framework". 14th ACM SIGPLAN International Conference on Functional Programming. doi:10.1145/1596550.1596591. 
  10. ↑ Cuoq, Pascal; Monate, Benjamin; Pacalet, Anne; Prevosto, Virgile; Regehr, John; Yakobowski, Boris; Yang, Xuejun (2012). "Testing Static Analyzers with Randomly Generated Programs". NASA Formal Methods, 4th International Symposium. 7226. Springer. pp. 120–125. doi:10.1007/978-3-642-28891-3_12. 
  11. ↑ "Toolchain Integration". https://trust-in-soft.com/toolchain-integration/. 
  12. ↑ "The TSnippet free online analyzer, free demo version of TrustInSoft Analyzer". https://tsnippet.trust-in-soft.com/. 
  13. ↑ "The TrustInSoft CI free online platform to analyze C and C++ code". https://ci.trust-in-soft.com/. 
  14. ↑ Moy, Yannick; Ledinot, Emmanuel; Delseny, Hervé; Wiels, Virginie; Monate, Benjamin (2013). "Testing or Formal Verification: DO-178C Alternatives and Industrial Experience". IEEE Software 30 (3): 50–57. doi:10.1109/MS.2013.43. 
  15. ↑ "Customers using TrustInSoft Analyzer". 2023. https://trust-in-soft.com/success_stories/. 
  16. ↑ "Elite French Auto Tech Companies Tour U.S., Eye CES". October 29, 2021. https://www.wardsauto.com/industry-news/elite-french-auto-tech-companies-tour-us-eye-ces. 
  17. ↑ "If You Can't Trust TrustInSoft, Who Can You Trust?". July 22, 2021. https://www.eejournal.com/article/if-you-cant-trust-trustinsoft-who-can-you-trust/. 
  18. ↑ "Finding code errors - mathematically". May 4, 2023. https://www-elektronikknett-no.translate.goog/innvevde-systemer-programvare-sikkerhet/finner-kodefeil-matematisk/3162290?_x_tr_sl=no&_x_tr_tl=en. 
  19. ↑ "How exhaustive static analysis improves software testing accuracy". July 25, 2023. https://www.embedded.com/how-exhaustive-static-analysis-improves-software-testing-accuracy/. 


Retrieved from "https://handwiki.org/wiki/index.php?title=Software:TrustInSoft_Analyzer&oldid=3195941"