Cryptol - język opisu algorytmów kryptograficznych
Cryptol stworzony przez firmę Galois jest językiem służącym do pisania specyfikacji algorytmów kryptograficznych w sposób ułatwiający analizę formalną, testowanie oraz weryfikację poprawności. Specyfikacja napisana w Cryptolu kompiluje się do VHDL, Haskella oraz C/C++.
Za darmo dostępna jest testowa wersja programu, darmowa do zastosowań niekomercyjnych. Firma Galois chwali się, że narzędzie zostało stworzone na potrzeby NSA. Więcej informacji na stronie Galois:
http://www.galois.com/technology/communications_security/cryptol
- Zaloguj się lub zarejestruj by odpowiadać
- Generate PDF file
- Wersja do wydruku
Odpowiedzi
W jakim sensie lepszy? Szybszy, mniej zasobochlonny i ladniejszy? To nie sa kryteria ktore sa istotne w tym wypadku. I oczywiscie automat nic nie pisze.
Celem jest mozliwosc uzyskiwania certyfikatu EAL7.
Koszt formalnej veryfikacji linijki kodu w C jest okolicach dziesieciu tysiecy dolarow jesli calosc nie przekracza kilku tysiecy linii. Powyzej tego szybko rosnie.
Cryptol to czesc stosu programow ktore maja na celu tworzenie oprogramowania i jego formalna veryfikacje. Stos wywodzi sie z projektu Programatica rozpoczetego przez zalozycieli Galois kiedy pracowali jeszcze na Oregon Health and Science University.
To swoją drogą nowy i bardzo ciekawie rozwijający się rynek. Ostatnio jak sprawdzałem listę certyfikatów CC udzielonych w ramach MRA to EAL7 miały ze 2-3 produkty o niezwykle prostej konstrukcji - np. dioda jednokierunkowa.
Wydaje mi się, że na EAL7 ma szansę wyłącznie produkt od zera zaprojektowany pod kątem certyfikacji, stąd na rynku pojawiają się narzędzia które ten proces usprawniają. Na przykład SPARK ADA, Cryptol czy narzędzia ułatwiające pisanie Security Targetu - np. polskie szablony TrustCase (Politechnika Gdańska).
Pewnie NSA, które z tego korzysta ma mniej zdolnych programistów
Niby ciekawy pomysł, ale to wymyślanie kolejnego narzędzia po to żeby pokazać to samo w inny sposób. Odniosłem wrażenie że ten nowy język dotyczy wyłącznie algorytmów symetrycznych. Wydaje mi się że mało zdolny programista jest w stanie napisać lepszy kod w C lub VHDL niż automat.