공식 사양과 검증
입증된 올바른 보안 모델을 사용하여 프로토콜을 개발하는 것의 중요한 강점은 적대적인 영향력이 제한되도록 보장한다는 것입니다. 프로토콜을 준수하고 증명이 정확하다면, 적대적 세력은 보안 속성을 위반할 수 없는 계약을 부여받습니다.
깊은 숙고는 이전 주장을 더 중요하게 만들어 줍니다. 적대세력은 얼마든지 지능적이고 유능할 수 있습니다. 그들을 단지 수학적인 모델을 통해 격퇴했다고 말하는 것도 대단합니다. 물론 그것이 모두 사실은 아니지만요.
현실에서는 순수한 보안과 올바른 행동이 존재할 수 없게 하는 많은 요인들과 환경들이 있습니다. 구현은 잘못될 수 있습니다. 하드웨어는 이전에는 고려하지 못했던 공격 방식이 나타나게 할 수 있습니다. 보안 모델이 미흡하여 실제에 적용하기 부적합할 수 있습니다.
프로토콜에 얼마나 많은 사양, 엄격함, 검사가 요구되는지 권위있는 판단이 필요합니다. 예를 들어, SeL4 Microkernel project 는 10,000줄 이하의 C코드의 모호성을 입증하기 위해서 200,000 줄의 isabelle 코드가 필요했던 주요 예시입니다. 그러나 운영 체제 커널은 제대로 구현되지 않으면 심각한 보안 취약점이 될 수있는 중요한 인프라입니다.
모든 암호학 소프트웨어들이 같은 수준의 엄청난 노력을 요구해야만 할까요? 또는 더 적은 비용으로 동일한 결과를 낼 수 있는 길을 선택할 수 있을까요? 만일 윈도우 XP 같이 취약하기로 악명 높은 환경에서라면 프로토콜이 완벽하게 구현되는 것이 중요할까요?
카르다노에서는 우리는 다음과 같은 절충안들을 선택했습니다. 첫째, 암호화 및 분산 컴퓨팅 영역의 복잡한 특성으로 인해 증명은 매우 미묘하고 길고 복잡하며 때로는 매우 기술적인 경향이 있습니다. 이는 인간이 주도하는 검사가 지루하고 오류가 발생하기 쉽다는 것을 의미합니다. 그러므로 우리는 핵심 인프라 구조를 다루는 백서에 적혀 있는 모든 중요한 증명은 컴퓨터에 의해 체크되야 한다고 생각합니다.
둘째, Haskell 코드가 우리 백서와 정확히 일치하는지 확인하기 위해서 LiquidHaskell를 통한 SMT 시험기를 가지고 인터페이싱하는 것과 Isabelle / HOL 사용 두 가지 옵션 중에서 선택할 수 있습니다.
SMT(적합성 모듈로 이론)는 방정식 또는 부등식을 만족시키는 기능 매개 변수를 찾는 문제를 처리하거나 그러한 매개 변수가 존재하지 않는다는 것을 보여줍니다. 드 모라 (De Moura)와 비요르너 (Bjørner)가 논의한 바와 같이 SMT의 용례는 다양하지만 요점은 이 기술이 모두 강력하고 버그와 오류를 매우 크게 줄일 수 있다는 점입니다.
반면에 Isabelle/HOL은 구현을 지정하거나 증명할 수 있는 더 표현적이고 다채로운 도구입니다. 이사벨 (Isabelle)은 고차원 논리 구조로 작업하는 일반 정리 증명으로, 증명에서 사용될 표현집합 및 기타 수학적 객체를 나타낼 수 있습니다. Isabelle 자체는 Z3 SMT 증명과 통합되어 이러한 제약 조건과 관련된 문제를 해결합니다.
두 가지 접근 방식 모두 의미 있는 것이기 때문에 우리는 두 가지 방식을 모두 단계적으로 채택하기로 결정했습니다. 사람의 서면 증명은 Isabelle으로 인코딩되어 정확성을 검사함으로써 기계 점검 요구 사항을 충족시킵니다. 그리고 우리는 2017, 2018년에 걸쳐서 카르다노 구현 코드에 Liquid Haskell을 점진적으로 추가할 것입니다.
마지막으로, 공식 검증은 그 검증의 기반이 되는 규격과 사용 가능한 도구들 만큼만 의미 있습니다. 하스켈을 선택하는 주된 이유 중 하나는 그것이 실재와 이론의 올바른 균형을 제공한다는 것입니다. 백서에서 파생된 명세는 하스켈 코드와 매우 흡사하고 두 가지를 연결하는 것은 명령형 언어를 사용하는 것보다 훨씬 쉽습니다.
적절한 명세를 파악하고 업그레이드, 버그 픽스 등 여러 변화가 생길 때 명세를 업데이트하는 것은 여전히 어려운 점이 많습니다. 하지만 이러한 현실이 전체적인 가치를 훼손하지는 않습니다. 입증 가능한 보안에 관해 기초를 구축하려 한다면, 그 구현은 실제로 논문에 제안된 것이어야 합니다.