Tiedoksi tietoturvasta ja erityisesti Common Criteria -arvioinnista kiinnostuneille NSA on julkaissut EAL5-tasolle sertifioidun esimerkkisovelluksen kokonaisuudessaan.
Kyseinen ohjelmisto lähdekoodeineen sekä dokumentaatioineen löytyy osoitteesta
http://www.adacore.com/home/gnatpro/tokeneer/
Lyhyesti: projekti toteutettiin käyttäen Praxis-nimisen brittiyrityksen Correctness-by-construction-menettelyä, joka perustuu pitkälti formaaleihin tai puoliformaaleihin menettelytapoihin. Toteutuskielenä projektissa oli SPARK, joka on erityisesti suunniteltu luotettavien, turvallisuuteen liittyvien ja tietoturvakriittisten sovellusten laadintaan.
Työkalut joilla projektin saa käännetyksi ovat myös vapaasti saatavilla.
Aihe on jo aika vanha, joten et voi enää vastata siihen.