1025: Automating the Formal Verification of Firmware: A Novel Foundation and Scalable Methodology

Electronic safety systems need to guarantee a certain level of dependability. Therefore, their development must consider not only robust hardware but also trustworthy and reliable embedded software such as firmware, drivers, and bare metal software. In the case of hardware, the use of formal verification and its automation are two crucial aspects to prevent the presence of bugs during the development process. However, formal verification of firmware and especially its automation lacks a methodology that can be applied to an industrial environment. In this paper, the verification of safety properties of firmware is automated to cover software criteria defined in the ISO26262-6 such as requirements-based tests, code coverage and weakness detection. Additionally, it introduces the main guidelines to enable this automation in an early phase of the development. The proposed methodology is based on the Model Driven Architecture and the generation of C files —usually called contracts. These files contain the functions under verification with the preconditions and post-conditions to be verified. This work considers an end-to-end register verification, which means that the design is proved concerning the Hardware Abstraction Layer (HAL). 

Furthermore, this work generates the scripts to run the open-source tool Bounded Model Checker for ANSI C (CBMC). In the beginning phase, the methodology was applied to verify the safety properties of industrial designs of 16 and 32 bits and after running some pilot projects, it was extended to automate the detection of weaknesses and code coverage. The results show that the generator can set up the verification environment in a few seconds and similar to hardware the verification runtime depends on the complexity of the design. The methodology can be easily adopted in industry or academic environments because it is based on Python scripts and open-source tools.