Feature: System security
soſtware lifecycle, and integrated into existing verification and validation processes for safety and security. One advantage of formal method tools over traditional static
analysis types is that developers can receive proof of absence of undefined behaviours in their code, thanks to the ability to quickly and efficiently perform billions of tests in one run.
Exhaustive static analysis In comparison to traditional testing methods and static analysis tools :(Figure 1), the technology of exhaustive static analysis uses advanced mathematical models to achieve up to 100% coverage of both code and inputs. Tis means that you can guarantee that all functions are tested and robust over the entire range of input values. In the automotive context, this means that you can reach soſtware structural and code coverage is strongly recommended by the ISO 26262 standard, and streamline the certification process. Exhaustive static analysis provides robustness and efficiency that gives developers the confidence to deliver code that is mathematically proven free of issues and functional safety risks. Tese exhaustive static analysis methods hinge on abstract
interpretation that simulates entire sets of given executions simultaneously, which significantly increases robustness by exponentially increasing the testing surface. In comparison to traditional tests that can only simulate individually for one given execution, exhaustive static analysis can, for example, perform 2,561,024 tests in one quick run. Using this approach, developers and testers can reach beyond the limits of traditional testing methods that can miss important and dangerous safety-critical bugs and vulnerabilities known as undefined behaviours. Exhaustive static analysis guarantees that the results of the
tests are valid for any compiler, the chosen set of compiler options, and any memory layout. Moreover, this method can be used for simultaneous analysis of extensive sets of input values. Hence, it removes the need for sequential or iterative testing with various input value sets, resulting in a substantial reduction in verification time. This automotive testing scope is achieved by using two
analysis levels: • Interpreter mode: the easiest and fastest to use and reuse existing test drivers when available. Tis mode identifies all undefined behaviours met when running the existing tests without false positives, and generates code coverage reports.
• Analyser mode: performs full exhaustive static analysis, without false negatives, accelerating the achievement of ISO 26262 objectives (e.g., boundary testing, robustness testing, etc.,), and generates code coverage reports.
Hardware awareness Te TrustInSoſt Analyzer improves the accuracy of its analysis by accounting for the actual compile and build toolchain and vehicle computing hardware. Users can specify characteristics like endianness, padding, memory mapping, memory alignment and floating-point-type size so that the analysis more accurately
Figure 1: Comparison of the execution paths between traditional testing (left) and exhaustive static analysis (right). Branches covered by one execution are represented in orange and unexplored segments are seen in black
represents the application’s runtime behaviour. For example: On 64-bit, non-Windows targets, long is typically 64 bits and int is typically 32 bits. On 32-bit targets, both long and int are typically 32 bits. Tese differences may cause integer overflows (a type of undefined behaviour) to occur in one target environment but not in others, even for the same code segment. Tis is shown in the following example:
long double_that(int i) { return (long)i * 2;
}
double_that(0x7FFFFFF0); Hardware awareness further provides the following
advantages: • Te execution of analysis is possible without requiring a physical target connected to the host system.
• Te initiation of target tests can occur at an earlier stage in the development cycle, even before the physical hardware becomes available.
• Test capacity can be expanded whilst simultaneously reducing costs, since there is no demand for physical hardware for every developer.
Finding buffer overflow with formal methods Undefined behaviours such as buffer issues have made embedded software developers’ lives very difficult. Buffer issues result from the bounds of allocated memory not being checked during the read and write operations. This causes the application to overflow beyond the capacity of the buffer, which impacts areas that aren’t intended for data extraction or modification. The following code sample illustrates a C function that increments cell values in an array:
www.electronicsworld.co.uk June 2024 13
Page 1 |
Page 2 |
Page 3 |
Page 4 |
Page 5 |
Page 6 |
Page 7 |
Page 8 |
Page 9 |
Page 10 |
Page 11 |
Page 12 |
Page 13 |
Page 14 |
Page 15 |
Page 16 |
Page 17 |
Page 18 |
Page 19 |
Page 20 |
Page 21 |
Page 22 |
Page 23 |
Page 24 |
Page 25 |
Page 26 |
Page 27 |
Page 28 |
Page 29 |
Page 30 |
Page 31 |
Page 32 |
Page 33 |
Page 34 |
Page 35 |
Page 36 |
Page 37 |
Page 38 |
Page 39 |
Page 40 |
Page 41 |
Page 42 |
Page 43 |
Page 44 |
Page 45 |
Page 46 |
Page 47 |
Page 48 |
Page 49 |
Page 50 |
Page 51 |
Page 52
