연구원 정보 및 자동화 연구를위한 주립 연구소 (인리아), Microsoft Research 및 Carnegie Mellon University 발표 의 첫 번째 평가판 EverCrypt 암호화 라이브러리 에베레스트 프로젝트 내에서 개발되었으며 공식적인 신뢰성 검증의 수학적 방법을 사용합니다.
그 기능과 성능을 위해 EverCrypt는 기존 암호화 라이브러리와 매우 가깝습니다. (OpenSSL) 그러나 그것은 그들과 달리 안정성과 보안에 대한 추가 보장을 제공합니다.
예 검증 프로세스는 세부 사양 정의로 귀결됩니다. 프로그램의 모든 동작을 설명하는 그리고 작성된 코드가 준비된 사양을 충족합니다.
증거 기반 품질 관리 방법과 달리 검증은 신뢰할 수있는 보증을 제공합니다. 프로그램은 개발자가 의도 한 대로만 실행되며 특정 종류의 오류는 없습니다.
예를 들어, 사양 준수 메모리와 함께 안전한 작업을 보장하고 버퍼 오버플로를 유발하는 오류 없음, 포인터를 역 참조하거나 이미 해제 된 메모리 영역에 액세스하거나 메모리 블록을 두 번 해제합니다.
EverCrypt는 무엇입니까?
에버크립트 강력한 유형 및 값 검사 제공-구성 요소는 다른 비준수 구성 요소에 매개 변수를 전달하지 않으며 다른 구성 요소의 내부 상태에 액세스 할 수 없습니다.
입력 / 출력 동작 간단한 수학 함수 동작을 완전히 준수, 암호화 표준에 정의되어 있습니다.
공격으로부터 보호하려면 타사 채널에서 계산 중 동작 (예 : 실행 기간 또는 특정 메모리에 대한 액세스의 존재) 처리되는 비밀 데이터에 의존하지 않습니다.
프로젝트 코드 기능적 언어 F *로 작성되었습니다. (F 스타) , 종속 유형 및 개선 시스템을 제공합니다., 프로그램에 대한 정확한 사양 (수학적 모델)을 설정하고 SMT 공식 및 보조 테스트 도구를 사용하여 구현시 오류의 정확성과 부재를 보장 할 수 있습니다.
F *의 코드는 Apache 2.0 라이선스에 따라 배포되고 최종 모듈은 C로 배포되고 어셈블러는 MIT 라이선스에 따라 배포됩니다.
참조 코드 F *를 기반으로, 어셈블러, C, OCaml, JavaScript 생성 및 웹 어셈블리 코드.
코드의 일부 준비된 프로젝트에 의해 이미 Firefox, Windows 커널에서 사용됨 , 블록 체인 Tezos 및 VPN Wireguard.
EverCrypt 구성 요소
본질적으로, EverCrypt는 HACL * 및 Vale에서 이전에 분리 된 두 개의 프로젝트를 결합합니다.,이를 기반으로 통합 API를 제공하고 실제 프로젝트에서 사용하기에 적합합니다.
HACL *은 Low로 작성됩니다.* 그리고 그 목표는 다음과 같은 C 프로그램에서 사용하기위한 암호화 기본 요소를 제공하는 것입니다. 그들은 libsodium 및 NaCL 스타일 API를 사용합니다.
프로젝트 Vale은 특정 언어를 개발했습니다. 어셈블러에서 확인을 생성하기위한 도메인입니다.
약 110 만 줄의 HACL * Low * 언어 코드와 25 만 XNUMX 천 줄의 Vale 코드가 결합되었습니다. 또한 범용 언어 F *로 약 70 만 줄의 코드로 다시 작성되었으며,이 역시 개발 중입니다. 에베레스트 프로젝트의 일환으로.
EverCrypt 라이브러리의 첫 번째 버전 검증 된 구현 기능 다음 암호화 알고리즘 중 C 또는 어셈블러 버전에서 제 안됨 (.
이 중 프로젝트 페이지에서 다음과 같은 사항이 두드러집니다.
- 해시 알고리즘 : SHA2, SHA3, SHA1 및 MD5의 모든 변형
- 인증 코드 : 데이터 소스 인증을위한 SHA1, SHA2-256, SHA2-384 및 SHA2-512를 통한 HMAC
- HKDF 키 생성 알고리즘 (HMAC 기반 추출 및 확장 키 유도 기능)
- ChaCha20 스트림 암호화 (최적화되지 않은 C 버전 사용 가능)
- Poly1305 MAC (Message Authentication Algorithm) (C 및 어셈블러 버전)
- 타원형 곡선 Curve25519에 대한 Diffie-Hellman 프로토콜 (BMI2 및 ADX 명령어를 기반으로 최적화 된 C 및 어셈블러 버전)
- 블록 암호 모드 AEAD (인증 된 암호) ChachaPoly (버전 C가 최적화되지 않음)
- AEAD AES-GCM 블록 암호화 모드 (AES-NI 최적화가 적용된 어셈블러 버전).
처음에는 알파 버전, 코드 검증이 이미 완료되었습니다. 하지만 여전히 일부 영역이 드러나지 않았습니다.
또한, API는 아직 안정화되지 않았습니다., 확장됩니다 다음 알파 버전에서 (모든 API에 대한 구조를 통합 할 계획입니다.
결함 중 x86_64 아키텍처에 대한 지원도 강조됩니다 (첫 번째 단계에서 주요 목표는 안정성이고 최적화 및 플랫폼은 두 번째로 구현됩니다).
출처 : https://jonathan.protzenko.fr