Software:TrustInSoft Analyzer: Difference between revisions

From HandWiki
(import)
 
(import)
 
Line 12: Line 12:
}}
}}


'''TrustInSoft Analyzer''' is a source code analyzer, analyzing code written in
'''TrustInSoft Analyzer''' is a source code analyzer that analyzes code written in the C and [[C++]] programming languages. It implements a set of various [[Formal methods|formal methods]], which create mathematical proofs of the absence of [[Undefined behavior|undefined behavior]] in the analyzed code.<ref>{{cite web
the C and [[C++]] programming languages. It implements a set of
|url= https://www.electronicdesign.com/technologies/embedded/software/video/21278213/electronic-design-trustinsoft-helps-root-out-bugs-to-deliver-reliable-code.
various [[Formal methods|formal methods]], which create mathematical proofs of the
|title=TrustInSoft Helps Root out Bugs to Deliver Reliable Code. |website= www.electronicdesign.com |date=29 November 2023 }}</ref>
absence of [[Undefined behavior|undefined behavior]] in the analyzed code. Undefined
behaviors are recognized as a major source of software vulnerabilities.<ref name="nist-8151">{{cite book
|author=National Institute of Standards and Technology
|title=Dramatically Reducing Software Vulnerabilities: NiSTIR 8151
|year=2016
|isbn=978-1548477714
|url=https://nvlpubs.nist.gov/nistpubs/ir/2016/NIST.IR.8151.pdf
|doi=10.6028/NIST.IR.8151
}}</ref>


Typical examples of undefined behavior, tracked by TrustInSoft
TrustInSoft Analyzer identifies undefined behavior including memory management issues such as [[Buffer overflow|buffer overflow]] and [[Uninitialized variable|uninitialized variable]]s, arithmetic operations including division by zero, [[Integer overflow|integer overflow]],and race conditions.<ref> {{cite web
analyzer, include memory management issues such as [[Buffer overflow|buffer overflow]]
and [[Uninitialized variable|uninitialized variable]]s; arithmetic operations including
division by zero and [[Integer overflow|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<ref name="nist-classification">{{cite web
|url=https://www.nist.gov/itl/ssd/software-quality-group/source-code-security-analyzers
|url=https://www.nist.gov/itl/ssd/software-quality-group/source-code-security-analyzers
|title=Source Code Security Analyzers
|title=Source Code Security Analyzers
|website=National Institute for Standards and Technology, Software Quality Group|date=23 March 2021
|website=National Institute for Standards and Technology, Software Quality Group|date=23 March 2021
}}</ref>
}}</ref>
including [[ISO 26262]] and [[MISRA C]].


The analyzer is not only limited to detect undefined behavior. It can
TrustInSoft Analyzer is commonly 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<ref>{{cite journal
also prove that a program conforms to a formal specification of its
|author=Benoit Jubin
intended functional behavior. The formal langage of specifications
|title=Exhausting
supported is the ANSI/ISO C Specification Language (ACSL).
|year=2023
|journal=Vehicle Electronics
|url= https://vehicle-electronics.biz/sites/default/files/VE118Oct23.pdf?mc_cid=14feb03339&mc_eid=3f3f5f6f4e
}}</ref>
including [[ISO 26262]] and [[MISRA C]].


== Basic Example of Use ==
It can also prove that a program conforms to a formal specification of its intended functional behavior including the ANSI/ISO C Specification Language (ACSL).


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


<syntaxhighlight lang="C" line> int absolute_int(long x) {
== Development and Deployment ==
  long abs_x;
  if (x < 0)
    abs_x = -x
  else
    abs_x = x;
  return abs_x;
}
</syntaxhighlight>


Running the analyzer will result in one alarm, positioned before
statement <syntaxhighlight lang="C" inline>abs_x = -x</syntaxhighlight> on  line 4, and categorized as a "signed overflow". The alarm is accompanied with an ACSL annotation as follows.
<syntaxhighlight lang="C"> //@ assert -x <= 9223372036854775807
</syntaxhighlight>
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 <syntaxhighlight lang="C" inline>x</syntaxhighlight>.




The user has the possibility to continue further by invoking another
TrustInSoft Analyzer deploys in multiple environments (e.g. Mac OS, Linux, Windows) and integrates with various tools (e.g. Google Test and Jenkins).<ref>{{cite web
level of analysis, which is going to try to prove that the assertion
|url= https://github.com/TrustInSoft
holds, using external theorem provers. In that case, not only the
|title= TrustInSoft
proof attempt will fail, but a potential counterexample is proposed,
|website=github.com}}</ref> All versions of C up to 18 and C++ up to 20 are supported.<ref>{{cite web
namely the value <syntaxhighlight lang="C" inline>0x80000000</syntaxhighlight> for <syntaxhighlight lang="C" inline>x</syntaxhighlight>. Indeed, this value denotes <syntaxhighlight lang="C" inline>LONG_MIN</syntaxhighlight>, the
|url= https://www.nist.gov/itl/ssd/software-quality-group/source-code-security-analyzers
smallest representable integer in the C type long, which denotes the integer
|title= Source Code Security Analyzers
-9223372036854775808, making the asserted assumption false.
|website=nist.gov|date= 23 March 2021
}}</ref>


It is indeed a classical example of a programming mistake, computing
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.<ref>{{cite web
the absolute value is not possible for <syntaxhighlight lang="C" inline>LONG_MIN</syntaxhighlight> 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.
 
<syntaxhighlight lang="C">/*@ requires x > LONG_MIN;
  @*/
int absolute_int(long x) {
</syntaxhighlight>
The given <syntaxhighlight lang="C" inline>requires</syntaxhighlight> clause is a [[Precondition|precondition]]. It means that the function should never be
called on the value <syntaxhighlight lang="C" inline>LONG_MIN</syntaxhighlight> for <syntaxhighlight lang="C" inline>x</syntaxhighlight>. 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 <syntaxhighlight lang="C" inline>absolute_int</syntaxhighlight> 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 [[Postcondition|postcondition]]s. For example, the same function could be given a more precise contract as follows.
<syntaxhighlight lang="C">/*@ requires x > LONG_MIN;
  @ ensures \result >= 0;
  @ ensures x >= 0 ==> \result == x;
  @ ensures x < 0 ==> \result == -x;
  @*/
int absolute_int(long x) {
</syntaxhighlight>
 
The other annotations, introduced by the ACSL keyword <syntaxhighlight lang="C" inline>ensures</syntaxhighlight> are
post-conditions. They declare that the given formulas hold at function
exit, where <syntaxhighlight lang="C" inline>\result</syntaxhighlight> denotes the result value of the function
call. These three post-conditions are indeed satisfied by the
function body for any input <syntaxhighlight lang="C" inline>x</syntaxhighlight>, and proved valid as such by TrustInSoft Analyzer.
 
== Overview of Implemented Technologies ==
 
TrustInSoft Analyzer applies various formal methods including
[[Abstract interpretation|abstract interpretation]] and [[Formal verification|deductive verification]] via the computation of [[Weakest precondition|weakest precondition]]s.  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.<ref>{{cite conference
|last1=Canet|first1=Géraud|last2=Cuoq|first2=Pascal|first3=Benjamin|last3=Monate
|title=A Value Analysis for C Programs
|year=2009
|conference=Ninth IEEE International Working Conference on Source Code Analysis and Manipulation
|doi=10.1109/SCAM.2009.22}}</ref>
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.<ref>{{cite conference
|first1=Pascal|last1=Cuoq|first2=Loïc|last2=Runarvot|first3=Alexander|last3=Cherepanov
|title=Detecting Strict Aliasing Violations in the Wild
|conference=Verification, Model Checking, and Abstract Interpretation
|year= 2017
|doi=10.1007/978-3-319-52234-0_2}}</ref>
To avoid a too large loss of precision when analysing code with conditional branches, it implements an original path-sensitive analysis.<ref>{{cite conference
|title=Result graphs for an abstract interpretation-based static analyzer
|last1=Cuoq|first1=Pascal|last2=Rieu-Helft|first2=Raphaël
|url=https://hal.science/hal-01503064
|conference=28th French Days on Functional Languages
|year=2017}}</ref> Moreover, when the analysis is not precise enough, the user has some ways to guide of the analysis.<ref>{{cite conference
|first1=Sven|last1=Mattsen|first2=Pascal|last2=Cuoq|first3=Sibylle|last3=Schupp
|title=Driving a sound static software analyzer with branch-and-bound
|conference=13th IEEE International Working Conference on Source Code Analysis and Manipulation
|pages=63–68
|publisher=IEEE Computer Society
|year=2013
|doi=10.1109/SCAM.2013.6648185}}</ref>
 
TrustInSoft Analyzer also implements deductive verification techniques to perform [[Formal proof|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 [[Predicate transformer semantics|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 [[Satisfiability Modulo Theories|SMT
solvers]] such as [[Software:Alt-Ergo|Alt-Ergo]] and Z3. Harder
proofs can be performed using the [[Software:Coq|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.<ref>{{cite journal
|first1=Pascal|last1=Cuoq|first2=Benjamin|last2=Monate|first3=Anne|last3=Pacalet
|first4=Virgile|last4=Prevosto
|title=Functional Dependencies of C Functions via Weakest Preconditions
|journal=International Journal on Software Tools for Technology Transfer
|volume=13|number= 5|pages=405–417
|year=2011
|doi=10.1007/s10009-011-0192-z|s2cid=24294899 }}</ref><ref>{{cite journal
|first1=Omar|last1=Chebaro|first2=Pascal|last2=Cuoq|first3=Nikolai|last3=Kosmatov
|first4=Bruno|last4=Marre|first5=Anne|last5=Pacalet|first6=Nicky|last6=Williams
|first7=Boris|last7=Yakobowski
|title=Behind the scenes in SANTE: a combination of static and dynamic analyses
|journal=Automation in Software Engineering
|volume=21|number=1|pages=107–143|year=2014
|doi=10.1007/s10515-013-0127-x|s2cid=254255861 }}</ref>
 
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.<ref>{{cite conference
|first1=Pascal|last1=Cuoq|first2=Julien|last2=Signoles|first3=Patrick|last3=Baudin
|first4=Richard|last4=Bonichon|first5=Géraud|last5=Canet|first6=Loïc|last6=Correnson
|first7=Benjamin|last7=Monate|first8=Virgile|last8=Prevosto|first9=Armand|last9=Puccetti
|title=Experience report: OCaml for an industrial-strength static analysis framework
|conference=14th ACM SIGPLAN International Conference on Functional Programming
|year=2009
|doi=10.1145/1596550.1596591}}</ref> Last but not least, the validity of the analyzer has been exercised through a heavy campaign of random testing,<ref>{{cite conference
|first1=Pascal|last1=Cuoq|first2=Benjamin|last2=Monate|first3=Anne|last3=Pacalet
|first4=Virgile|last4=Prevosto|first5=John|last5=Regehr|first6=Boris|last6=Yakobowski
|first7=Xuejun|last7=Yang
|title=Testing Static Analyzers with Randomly Generated Programs
|conference=NASA Formal Methods, 4th International Symposium
|series=Lecture Notes in Computer Science
|volume=7226
|pages=120–125
|publisher=Springer
|year=2012
|doi=10.1007/978-3-642-28891-3_12}}</ref> 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
[[Software:Frama-C|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).<ref>{{cite web
|url=https://trust-in-soft.com/toolchain-integration/
|title=Toolchain Integration
|website=trust-in-soft.com}}</ref>
All versions of C up to 18 and C++ up to 20 are supported.<ref name="nist-classification"/>
 
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.<ref>{{cite web
|url=https://tsnippet.trust-in-soft.com/
|url=https://tsnippet.trust-in-soft.com/
|title=The TSnippet free online analyzer, free demo version of TrustInSoft Analyzer
|title=The TSnippet free online analyzer, free demo version of TrustInSoft Analyzer
|website=trust-in-soft.com}}</ref> 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.<ref>{{cite web
|website=trust-in-soft.com}}</ref> Additionally, another free, fairly complete, version of the analyzer is available on the web, able to analyze code if the source is publicly hosted on Github.<ref>{{cite web
|url=https://ci.trust-in-soft.com/
|url=https://ci.trust-in-soft.com/
|title=The TrustInSoft CI free online platform to analyze C and C++ code
|title=The TrustInSoft CI free online platform to analyze C and C++ code
|website=trust-in-soft.com}}</ref>
|website=trust-in-soft.com}}</ref>


== Applications and Visibility ==
== Applications and Visibility ==


Together with its ancestor Frama-C, TrustInSoft Analyzer has been used in several industrial-scale applications.<ref>{{cite journal
TrustInSoft Analyzer’s technology, previously developed under Frama C, has industrial-scale applications to formally verify critical aeronautic applications such as DO-178C.<ref>{{cite journal
|first1=Yannick|last1=Moy|first2=Emmanuel|last2=Ledinot|first3=Hervé|last3=Delseny
|first1=Yannick|last1=Moy|first2=Emmanuel|last2=Ledinot|first3=Hervé|last3=Delseny
|first4=Virginie|last4=Wiels|first5=Benjamin|last5=Monate
|first4=Virginie|last4=Wiels|first5=Benjamin|last5=Monate
Line 226: Line 64:
|volume=30|number=3|pages=50–57|year=2013
|volume=30|number=3|pages=50–57|year=2013
|doi=10.1109/MS.2013.43|s2cid=12345793 }}</ref>
|doi=10.1109/MS.2013.43|s2cid=12345793 }}</ref>
The web site of TrustInSoft maintains a list of successful industrial applications.<ref>{{cite web
TrustInSoft has since expanded into markets such as consumer electronics and automotive.<ref>{{cite web
|title=Customers using TrustInSoft Analyzer
|url=https://www.cea.fr/english/Pages/innovation/start-ups/trustinsoft.aspx
|url=https://trust-in-soft.com/success_stories/
|title=Trustinsoft, quality and security for C & C++ software
|year=2023
|date=December 15, 2022
|website=TrustInSoft company}}</ref> In 2016, TrustInSoft Analyzer was accredited in a NIST report to the White
|website= Le CEA}}</ref> 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 (now referred to as Mbed_TLS) stack.<ref>{{cite book
House Office of Science and Technology Policy, for proving the absence of CWE vulnerabilities in the
|author=National Institute of Standards and Technology
PolarSSL (nowadays known as [[Software:Mbed TLS|Mbed TLS]]) stack.<ref name="nist-8151"/> In 2021,
|title=Dramatically Reducing Software Vulnerabilities: NiSTIR 8151
TrustInSoft was selected by UBIMobility, an accelerator for
|year=2016
autonomous vehicles technologies.<ref>{{cite web
|isbn=978-1548477714
|url=https://nvlpubs.nist.gov/nistpubs/ir/2016/NIST.IR.8151.pdf
|doi=10.6028/NIST.IR.8151
}}</ref>
In 2021, TrustInSoft was selected for the UBIMobility development program, an accelerator for autonomous vehicle technologies.<ref>{{cite web
|url=https://www.wardsauto.com/industry-news/elite-french-auto-tech-companies-tour-us-eye-ces
|url=https://www.wardsauto.com/industry-news/elite-french-auto-tech-companies-tour-us-eye-ces
|title=Elite French Auto Tech Companies Tour U.S., Eye CES
|title=Elite French Auto Tech Companies Tour U.S., Eye CES
|date=October 29, 2021
|date=October 29, 2021
|website=Wards Automotive, Industry News}}</ref>
|website=Wards Automotive, Industry News}}</ref>
TrustInSoft Analyzer acquired some world-wide visibility in the press specialized in electronic and software engineering.<ref>{{cite web
|url=https://www.eejournal.com/article/if-you-cant-trust-trustinsoft-who-can-you-trust/
|title=If You Can't Trust TrustInSoft, Who Can You Trust?
|date=July 22, 2021
|website=Electronic Engineering Journal}}</ref><ref>{{cite web
|url=https://www-elektronikknett-no.translate.goog/innvevde-systemer-programvare-sikkerhet/finner-kodefeil-matematisk/3162290?_x_tr_sl=no&_x_tr_tl=en
|title=Finding code errors - mathematically
|date=May 4, 2023
|website=Elektronikknett, Norway}}</ref><ref>{{cite web
|url=https://www.embedded.com/how-exhaustive-static-analysis-improves-software-testing-accuracy/
|title=How exhaustive static analysis improves software testing accuracy
|date=July 25, 2023
|website=Embedded}}</ref>
==See also==


* [[Static program analysis]]
* ANSI/ISO C Specification Language
* [[Formal verification]]
* [[Software:Frama-C|Frama-C]] software environment


== References ==
== References ==
{{Reflist}}
{{Reflist}}
{{Sourceattribution|TrustInSoft Analyzer}}
{{Sourceattribution|TrustInSoft Analyzer}}

Latest revision as of 13:48, 26 April 2024

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 that analyzes 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.[1]

TrustInSoft Analyzer identifies undefined behavior including memory management issues such as buffer overflow and uninitialized variables, arithmetic operations including division by zero, integer overflow,and race conditions.[2]

TrustInSoft Analyzer is commonly 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[3] including ISO 26262 and MISRA C.

It can also prove that a program conforms to a formal specification of its intended functional behavior including the ANSI/ISO C Specification Language (ACSL).


Development and Deployment

TrustInSoft Analyzer deploys in multiple environments (e.g. Mac OS, Linux, Windows) and integrates with various tools (e.g. Google Test and Jenkins).[4] All versions of C up to 18 and C++ up to 20 are supported.[5]

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.[6] Additionally, another free, fairly complete, version of the analyzer is available on the web, able to analyze code if the source is publicly hosted on Github.[7]

Applications and Visibility

TrustInSoft Analyzer’s technology, previously developed under Frama C, has industrial-scale applications to formally verify critical aeronautic applications such as DO-178C.[8] TrustInSoft has since expanded into markets such as consumer electronics and automotive.[9] 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 (now referred to as Mbed_TLS) stack.[10] In 2021, TrustInSoft was selected for the UBIMobility development program, an accelerator for autonomous vehicle technologies.[11]


References

  1. ↑ "TrustInSoft Helps Root out Bugs to Deliver Reliable Code.". 29 November 2023. https://www.electronicdesign.com/technologies/embedded/software/video/21278213/electronic-design-trustinsoft-helps-root-out-bugs-to-deliver-reliable-code.. 
  2. ↑ "Source Code Security Analyzers". 23 March 2021. https://www.nist.gov/itl/ssd/software-quality-group/source-code-security-analyzers. 
  3. ↑ Benoit Jubin (2023). "Exhausting". Vehicle Electronics. https://vehicle-electronics.biz/sites/default/files/VE118Oct23.pdf?mc_cid=14feb03339&mc_eid=3f3f5f6f4e. 
  4. ↑ "TrustInSoft". https://github.com/TrustInSoft. 
  5. ↑ "Source Code Security Analyzers". 23 March 2021. https://www.nist.gov/itl/ssd/software-quality-group/source-code-security-analyzers. 
  6. ↑ "The TSnippet free online analyzer, free demo version of TrustInSoft Analyzer". https://tsnippet.trust-in-soft.com/. 
  7. ↑ "The TrustInSoft CI free online platform to analyze C and C++ code". https://ci.trust-in-soft.com/. 
  8. ↑ 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. 
  9. ↑ "Trustinsoft, quality and security for C & C++ software". December 15, 2022. https://www.cea.fr/english/Pages/innovation/start-ups/trustinsoft.aspx. 
  10. ↑ 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. 
  11. ↑ "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. 


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