-
Notifications
You must be signed in to change notification settings - Fork 0
Testing the Native Component
This document describes the testing of the Native Component.
The functionality consists of CIFF parsing and conversion and CAFF parsing and conversion which builds on the CIFF parsing part. Thereby our functionality testing is also twofold, first, testing the CIFF parsing capabilities, then testing the CAFF parsing feature.
The functionality of the CIFF parsing is tested via different CIFF files that target the different features of the code.
The tests are implemented in the ciff_test.hpp file in the check_ciff
function. The function takes a CIFF file route and parses it. If the parsing has been successful, it converts the ciff to BMP, then frees the memory.
The functionality of the CAFF parsing is tested via different CIFF files that target the different features of the code.
The tests are implemented in the caff_test.hpp file in the check_caff
function. The function takes a CAFF file route and parses it. If the parsing has been successful, it converts the ciff to BMP, then frees the memory.
The fuzzing of the CAFF parser also was a two-part job. First, we fuzzed the CIFF parser, then the CAFF parser. For the fuzzing, we used AFL.
To fuzz the CIFF parser, we created a helper program, that takes the file to parse as a command line argument, parses the CIFF file and then converts it to BMP if the parsing is successful.
The logs of the fuzzing can be downloaded from here. AFL generated 108 different inputs which can be seen in the ciff-fuzz folder. The most important statistics of the fuzzing are listed below:
Parameter | Value |
---|---|
Command | afl-fuzz -i test/fuzz_in -o test/fuzz_ciff_out/ bin/ciff-cli @@ |
Paths total | 108 |
Execs done | 2154473 |
Duration | 1 hour 5 minutes |
Number of crashes | 0 |
Number of hangs | 0 |
To fuzz the CAFF parser, we created a helper program, that takes the file to parse as a command line argument, parses the CAFF file and then converts it to BMP if the parsing is successful.
The logs of the fuzzing can be downloaded from here. AFL generated 72 different inputs which can be seen in the caff-fuzz folder. The most important statistics of the fuzzing are listed below:
Parameter | Value |
---|---|
Command | afl-fuzz -i test/fuzz_in -o test/fuzz_caff_out/ bin/caff-cli @@ |
Paths total | 72 |
Execs done | 2211327 |
Duration | 1 hour 5 minutes |
Number of crashes | 0 |
Number of hangs | 0 |
We used CPAChecker to formally verify properties of our parser. The entry point of the formal verification was the CAFF helper program.
We executed the CPAChecker with the following commands and results. All the verification tasks run for 1 hour, with the memory limit of 4 GB on 4 cores of 3.1 GHz.
The command we used: scripts/cpa.sh -config config/default.properties -spec config/specification/[spec] <source files>
Spec | Target property | Result |
---|---|---|
overflow.spc | Checks whether operations can overflow in the program | UNKNOWN |
null-deref.spc | Checks whether the NULL pointer is dereferenced in the program | SAFE |
memorysafety.spc | Checks whether the memory is used correctly (every allocated byte is freed, there are no read of uninitialized memory, etc...) | UNKNOWN |
termination_as_reach.spc | Checks whether the program can hang indefinitely | SAFE |
This section contains the evaluation of the testing of the native component.
Using the functional tests implemented by the team and the tests generated via fuzzing, the tests reach a decent coverage of 89.2%.
Further analyzing the coverage, it can be seen, that the missed instructions in the CIFF parser correspond to the error handling of running out of memory. The same can be observed in the case of the CAFF parser.
Overall, we conclude that we tested every major aspect of the native parser.
Out of the four verified property, only two was successful. Based on the verification we concluded that:
- The implementation never dereferences a NULL pointer.
- The implementation always terminates, cannot hang algorithmically.
The other two properties failed to verify within the time range, however based on the time limit and the verification algorithm in use, it is reasonable to assume that:
- Overflow can only happen on a non-trivial path (e.g. the special correlation of multiple conditions)
- Memory management errors can only happen on a non-trivial path (e.g. the special correlation of multiple conditions)
© Grotesque Gecko, 2020
- Functional Requirements and Use Cases
- Security Requirements and Objectives
- Threat Assessment
- Quality Gates
- Chosen Technologies
- Required Security Functionalities
- Structural Model of the System
- Behavioral Model of the System