In July 2023, SERMA SAFETY & SECURITY acquired SafeRiver to enhance its expertise in formal methods, thereby strengthening its established position in Dependability and Cybersecurity.
For nearly 20 years, SafeRiver has developed expertise in implementing formal methods for critical systems and software across the railway, automotive, and defense sectors.
SafeRiver’s doctors and engineers contribute early in the development cycle—from defining behavioral properties to identifying weaknesses and vulnerabilities—on projects with high levels of dependability or cybersecurity.
To support its consulting and expertise activities, SafeRiver has developed SafeProver—a Model-Checking tool certified as T2 for the railway sector—and IFFREE, software used to assess the absence of impact between modules/software of different criticality levels.
The services and tools provided by SafeRiver offer increased confidence in:
- architectural decisions,
- the comprehensiveness of test scenarios,
- the reproducibility of verification,
- the absence of impact between different criticality flows (safety/non-safety),
- and maintainability throughout the product life cycle.
WHAT are formal methods ?
Formal methods refer to a set of mathematical techniques used to specify, design, and verify systems with a strong software and electronic component. Unlike traditional verification methods based on empirical testing, formal methods allow for the mathematical proof that the system satisfies certain specified properties.
Several studies have shown that the use of formal methods leads to a significant reduction in overall costs (development costs, verification costs, maintenance costs) for critical systems.
Formal methods are deployed to address issues such as:
of Safety
- Formal methods allow for the precise definition of dependability requirements using mathematical models.
- They enable the formal demonstration that the system meets the specified safety properties.
- By modeling and analyzing the system early in the development stages, design errors that could affect safety can be detected and corrected before the system is even implemented.
- In many industries, such as aerospace, automotive, or railways, dependability standards (IEC 61508, EN 50128, ISO 26262, …) recommend the use of formal methods for certain categories of critical systems.
of Cybersecurity
- Formal methods are recommended or even required, for example, in the context of Common Criteria certification for high security levels (from EAL 4+).
- The underlying mathematical approaches (such as typing, abstract interpretation, or model checking) help ensure the absence of certain categories of errors. The use of formal methods can be applied during the specification, design, implementation, and testing phases.
- Well-known methods such as B and COQ can be used.
Services
SafeRiver has developed a specific offering to assess the security of systems and software by implementing formal methods.
Offering related to safety
Security Analysis (FHA)
- Identification of security criteria
- Development of observable security properties
- Coverage of system mitigation measures
Formal Verification of Models
- Compliance with security properties
- Absence of execution errors
- Model checking or theorem proving
Static Code Analysis
- Detection of execution errors
- Detection of dead code and blocking
- Verification of coding standards
Co-simulation
- Equivalence between model and code
Test Generation
- Automatic generation of test cases from security properties
Offering related to cybersecurity
Methodological Kits for Language Security
- Design rules for secure use of languages
- Recommendations for code production
Static Analysis for Security
- Configuration profiles of static analysis tools (e.g., Polyspace, Coverity, Klocwork, …) with CWE
- Detection of vulnerabilities
- Risk assessment related to vulnerabilities and flaws
- Control flow, data flow, and interface usage accuracy (i.e., absence of interference)
Evaluation of Static Analysis Tools for Security
- Juliet-based evaluation kit
- ANSSI/DGA project (LaboSSec, AMOEASU)
Products
SAFEPROVER Tool
SAFEPROVER is a model-checking tool qualified at Level T2 for SIL4 applications in compliance with the EN50128 and IEC 62279 (Clause 6.7) standards. This tool is used for the formal verification of safety-related behavioral properties in software systems.
IFFREE Tool
The IFFREE tool is a static analysis tool for C code, designed to detect interferences between codes with different integrity levels. Since 2015, it has been used in automotive applications to meet the requirements of the ISO 26262 standard (Freedom From Interference).