이달 초 Blockstream은 블록체인 언어 Simplicity에 대한 소스 코드를 발표했습니다.
Simplicity는 블록체인 환경에서 복잡한 스마트 계약의 코딩을 시도할 때 직면하는 문제에 대한 Blockstream의 해결책입니다. Simplicity가 나오기 전, 블록체인 프로그래밍 언어는 대체로 표현성과 신뢰성 사이에서 절충을 이루었습니다; 개발자들은 복잡하지만 신뢰할 수 없는 스마트 계약 또는 굉장히 기본적이지만 신뢰할 수 있는 계약을 만들 수 있었습니다. 하지만 이제 Simplicity를 사용하면 복잡한 스마트 계약을 설계하고 그 결과를 확신할 수 있습니다.
Simplicity는 Blockstream의 Elements 플랫폼과 호환되도록 구축되었습니다. 즉, Elements에 사이드체인이나 독립 블록체인을 구축하는 개발자들은 조만간 Simplicity가 지원하는 기능을 활용할 수 있을 것입니다. Liquid Network도 Elements의 구현으로서 Simplicity를 지원할 것입니다; 신뢰가 최소화된 에스크로(escrow), 금고(vault), 그리고 더욱 복잡한 스마트 계약 등 Liquid 사용자를 위한 흥미로운 응용 프로그램이 제공될 것입니다.
이번 달에 발표된 소스는 다음과 같습니다:
● 핵심 Simplicity 언어의 표시론적 의미론과 Coq에 공식 지정된 확장 프로그램.
● Coq에 공식 지정된 핵심 Simplicity 언어의 연산 의미론.
● Haskell로 작성된 Simplicity 언어의 해석 프로그램(interpreter), 유형 검사자(type-checker), 직렬화.
● SHA-256 및 EC-Schnorr 서명 검증 같은 암호화 작업을 포함한 Simplicity 표현의 예.
● Simplicity 언어를 상술한 기술 보고서.
왜 Simplicity인가?
블록체인은 전통적인 프로그래밍 언어를 부적합하게 만드는 몇 가지 특이한 문제를 야기합니다.
● 모든 사용자는 모든 환경에서 연산 결과에 동의해야 합니다.
● 스마트 계약의 각 참여자는 프로그램에 대한 모든 가능한 입력에 대해 가능한 모든 결과를 미리 알고 있어야 합니다.
● 모든 사용자는 과도한 메모리나 연산 시간을 소비할 수 있는 DoS(서비스 거부 공격)을 방지할 수 있어야 합니다.
● 스마트 계약의 각 참여자는 가능한 모든 입력에 대한 프로그램 실행 비용을 미리 알 수 있어야 합니다.
Ethereum의 EVM 등 블록체인을 위해 특별히 설계된 기존 프로그래밍 언어는 여전히 이러한 문제를 갖고 있습니다. 최근, 구현과 연산 결과가 부합하지 않았기 때문에 테스트 중 EVM 업그레이드가 실패했습니다. 스마트 계약 논리 오류와 리소스 한도를 초과하는 프로그램으로 인해 자금이 도난됐거나 복구가 불가능해졌습니다.
하지만, 일반적으로 비트코인의 Script 언어는 디지털 서명 확인, 타임락, 해시락의 조합으로 제한됩니다. (Lightning Network 같은) 우수한 프로토콜은 이러한 기본 요소를 기반으로 구축되어 왔지만 비트코인의 Script 언어는 더욱 복잡한 스마트 계약에 필요한 표현성이 부족합니다.
Simplicity의 목표는 필요한 모든 연산에 유연성과 표현성을 제공하고 사용자가 스마트 계약의 안전성, 보안, 그리고 비용을 검증할 수 있도록 하는 것입니다.
Simplicity란?
Simplicity는 블록체인 기반의 스마트 계약을 위한 저급 프로그래밍 언어이자 머신 모델입니다. 이는 처음부터 형식적인 방법에 의한 정적 분석과 추론에 적합한 단순 의미론을 갖도록 설계되었습니다. Simplicity 언어는 Coq 증명 보조기에서의 구현으로 정의됩니다.
이 핵심 언어 자체는 티셔츠에 문구로 넣을 수 있을 정도로 단순하지만, 언어가 단순하다고 해서 개발이 간단한 것은 아닙니다. 그 이유는 다음과 같습니다:
● 블록체인은 일반 프로그래밍과는 근본적으로 다른 프로그래밍 모델을 포함합니다. 블록체인의 역할은 연산을 수행하는 것이 아니라 연산을 검증하는 것입니다. 이것은 미묘한 차이이지만, 튜링 완전(Turing-completeness) 없이도 임의의 코드 실행을 검증할 수 있기 때문에 매우 중대한 차이입니다.
● 일단 배포되고 나면 스마트 계약은 변경할 수 없기 때문에 오류를 고칠 수가 없습니다. Simplicity는 사용자가 스마트 계약에 대한 공식적인 정확성 증명을 만들 수 있도록 함으로써 이러한 문제를 해결합니다.
● Simplicity는 직접 실행을 위한 매우 낮은 수준의 언어로, Java 또는 Python보다는 어셈블리어와 유사합니다. 궁극적으로 우리는 사용자가 계약을 하나 이상의 고급 언어로 작성한 뒤 Simplicity로 컴파일할 것으로 예상합니다.
최근 소식
Simplicity에 대한 글을 블로그에 마지막으로 게시한 이후, Blockstream은 실험어 연구를 보다 형식적인 언어 사양으로 발전시키기 위해 열심히 노력해 왔습니다.
그리고 다음과 같이 Coq 증명 보조기에서 Simplicity 언어를 재구현했습니다:
● Blockstream은 witness 데이터, 주장(assertion), 및 위임(delegation)을 지원하는 언어 확장 프로그램을 포함한, 전체 Simplicity 언어의 표시론적 의미론을 갖고 있습니다.
● 무료 카테고리를 기반으로 한 “the Bit Machine”이라 불리는 추상 머신의 공식 사양은 핵심 Simplicity 언어에 대한 연산 의미론을 제공합니다.
● 태그 없는 최종 스타일로 개발된 Haskell 구현을 사용하면 Simplicity 표현의 평가, 실행, 유형 검사를 시험할 수 있습니다.
● Simplicity 언어 확장 프로그램에 대한 모듈식 접근 방법을 활용하면 언어 확장 프로그램을 사용하지 않을 때 프로그램의 영향을 무시할 수 있습니다.
● Blockstream은 자체적으로 Simplicity에서 libsecp256k1를 재구현하는 등 암호화 원시 요소(primitive)에 대한 Simplicity 표현을 다수 보유하고 있습니다.
● Simplicity 언어에 대한 비공식적 수학적 사양을 제공하고 Coq 및 Haskell 개발에 대한 가이드를 제공하는 기술 보고서.
Simplicity 개발은 여전히 진행 중이지만, Blockstream의 개발자들은 이제 Simplicity 언어 자체를 탐색할 수 있는 수준까지 도달했습니다. 따라서 이제는 Simplicity 개발을 오픈으로 옮기고 메일링 리스트를 열 때가 되었습니다.
다음 단계
앞으로 Simplicity 개발은 많은 영역에서 이루어질 것입니다.
Blockstream의 개발 계획은 다음과 같습니다:
● C 해석 프로그램 완성.
● 다양한 일반적인 암호화 기능을 위한 제트 라이브러리 구현.
● 검증 가능한 C를 사용하여 C 해석 프로그램과 제트가 올바른지 증명.
● Elements 블록체인 플랫폼에 Simplicity 통합.
개발의 다른 영역은 다음과 같습니다:
● Simplicity 코드 최적화 도구 개발.
● Simplicity 생성을 위해 Ivy와 같은 새로운 고급 스마트 계약 플랫폼을 만들거나 기존 플랫폼 적용.
● Simplicity의 암호화 원시 요소의 기능적 정확성과 암호화 프로토콜의 공식적 정확성을 결합하여 완전히 검증된 스마트 계약 구축.
Blockstream의 프로젝트에 함께해 주시기 바랍니다.