On Using B in the Design of Secure Micro-controllers: An Experience Report

The stepwise formal development of safety critical software is now a well established engineering practice, noticeably in railway systems. However, it has not been applied as successfully to hardware development, where formal methods are mainly used for verification and gate level transformations and optimizations. In this paper, we report our recent experience in the stepwise formal development of a real macro-cell, that opens the way to the design of synchronous digital circuits with zero functional bugs. We propose a development flow suited for obtaining proven correct-by-construction circuits that further possess additional robustness properties desirable for secure chips. The reported work is prospective and is meant to show the feasibility of such a technique for high confidence trustful devices.