[SC-L] How Can You Tell It Is Written Securely?

[ljknews]

At 9:03 PM -0500 11/26/08, Mark Rockman wrote:

> OK.  So you decide to outsource your programming assignment to Asia and
>demand that they deliver code that is so locked down that it cannot
>misbehave.  How can you tell that what they deliver is truly locked down?
>Will you wait until it gets hacked?  What simple yet thorough inspection
>process is there that'll do the job?  Doesn't exist, does it?

Certainly it exists.  Rerun the verification of the formal proof,
as used in the Tokeneer project I mentioned earlier.

Of course a formal proof only proves that software conforms to
a specification, so unless you have a specification you have
nothing, and that is what a lot of software is lacking.
-- 
Larry Kilgallen