저수준 제어와 코드 구조
암호 코드는 결과가 맞는 것뿐 아니라 기계에서 실행되는 방식도 중요하다. Jasmin은 명령 선택과 레지스터 사용 같은 성능 관련 결정을 다루면서, 변수와 반복문 등으로 프로그램 구조를 표현한다. 수작업 어셈블리와 고수준 코드 사이의 간격을 줄이는 접근이다.
서로 다른 검증 대상
안전성 검사, 종료성 분석, 함수의 계산 결과에 대한 증명은 구분되는 작업이다. 컴파일러 정확성에 대한 증명도 구현하려는 암호 알고리즘 자체의 안전성을 대신하지 않는다. 어떤 성질을 어느 단계에서 확인했는지 구체적으로 살펴야 한다.
암호 분석과 연결
프로그램을 EasyCrypt 표현으로 추출해 기능적 정확성이나 암호학적 성질을 분석할 수 있다. 비밀값에 따라 실행 시간이 달라지는 문제 역시 별도의 검증 관심사다. 언어를 사용했다는 사실만으로 모든 부채널 위험이 사라지는 것은 아니다.