Position:Security Viewpoint

CEA ( Commissariat a l'Energie Atomique) in France have developed Caveat, an innovative software tool that enhances safety control in critical software in industrial applications. Caveat mainly detects errors due to the software not having the expected characteristics. It also examines the possibility of errors in the function of the software such as infinite loops and division by zero. Its principle of operation consists in comparing the software to be verified, which can consist of some tens of thousands of lines of code for example, with the functional result expressed by a mathematical formula only a few lines in length. From this comparison, Caveat formulates a mathematical condition: for example, for the result to be as expected, the parameter 'a' must be less than zero. The user then verifies that this parameter is less than zero in all cases. If so, this is taken as proof that the result corresponds to an expected property. If the proof fails, the tool gives indications as to the masons for the failure. In most eases, this will be due to initial assumptions, which then need to be...

To continue reading