Testing the Native Component

This document describes the testing of the Native Component.

Functional Testing

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.

CIFF parsing

The functionality of the 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.

CAFF parsing

The functionality of the 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.

Fuzzing

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.

CIFF fuzzing

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|TestingDocs/fuzz_ciff.zip]. 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

CAFF fuzzing

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|TestingDocs/fuzz_caff.zip]. 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

Formal verification

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

Evaluation

This section contains the evaluation of the testing of the native component.

Testing

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.

Formal verification

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)