Design methodologies

Certified CAD tools
Sensitive designs can be strengthened by a variety of transformations that increase their security level. Secure-IC develops source-to-source compilers, that can thus be used in conjunction with any legacy design flow. Paramount is the guarantee that the tool actually achieves what it is asked to, no more, no less. Such a warranty is ensured by the certification of the CAD tools; the most security critical of them are extracted automatically by COQ and are thus proved to adhere exactly to their function. The extraction results in a program in OCAML, i.e. a correct by design language, free of any bug. This allows to kill two birds with one stone: the tool ensures a non-regression and is itself checked for the absence of backdoors.

Formally provable secure IPs
CAD tools allow automating the design of secure IPs. Now, worrying whether the transformations actually elevate the security level is a sane preoccupation. The approach promoted by Secure-IC relies on a careful modelization of the system and of its security properties, in a formal framework. Thanks to this formal description, the intended security features of the countermeasure are checked for consistency with their descriptions. Thus, the countermeasures embedded in secure IPs are indeed proved useful.