반복의 기술
암호통화는 소프트웨어로 구현된 프로토콜(규약)입니다. 프로토콜이란 참가자들 간의 지능형 의사소통을 말합니다. 소프트웨어는 궁극적으로 주어진 목표에 따라 데이터를 조작하는 것입니다. 하지만 유용하고 안전한 프로토콜을 가질 뿐만 아니라, 안정적하고 신뢰할 수 있는 소프트웨어와 그 반대와의 차이점은 오직 사람에 달려있습니다.
훌륭한 소프트웨어는 신뢰성, 명확한 비즈니스 요구 사항과 반복 가능한 프로세스 그리고 철저한 테스트 및 지칠 줄 모르는 반복을 필요로 합니다. 또한 훌륭한 소프트웨어는 문제를 완전히 해결할 수 있는 시스템을 설계하기에 충분한 도메인 지식을 가진 재능있는 개발자가 필요합니다.
유용하고 안전한 프로토콜, 특히 암호화 및 분산 시스템과 관련된 프로토콜은 보다 학문적이고 표준 지향적인 프로세스로 시작됩니다. 유용한 프로토콜을 확립하기 위해서는 동료의 리뷰, 끝없는 토론 그리고 트레이드 오프에 대한 확고한 개념이 필요합니다. 그러나 이것들 만으로 충분하지 않습니다. 프로토콜은 현실에서 사용되어지고 테스트 되어져야 합니다.
암호통화 산업에서 특별히 어려운 점은 두 개의 완전히 다른 철학이 적절한 변증법적 합의 없이 뒤섞여 있다는 점입니다. “빠르게 변화하고 목표를 성취하는 것”같은 젊음과 야망 그리고 열정으로 움직이는 스타트업 정신이 우리의 정명제입니다. 반명제는 암호화폐 영역에서의 혁신들을 충분한 펀딩과 명성을 누리는 훌륭한 위치에 정착시키고자 하는 욕구에서 나오는 것으로, 느리고 체계적이며 학술 지향적인 접근 방식입니다.
결과적으로 많은 암호통화들은 오직 개념 검증에만 관련된 백서 또는 급하게 작성된 코드에 의해 완전히 특정지어 집니다. 현재 시가총액 상위 10대18 암호화폐 중 어떤 것도 상호 검증한 프로토콜에 근거하지 않습니다. 그리고 현재 상위 10대 암호화폐들 모두 공식적인 규격에 기반하여19 구현되지 않았습니다.
그러나 수십억 달러의 가치가 위험에 빠져있습니다. 한번 배포가 되면 암호통화는 변경하기가 매우 어렵습니다. 그렇다면 어떻게 사용자는 그들이 안전한 시스템을 사용하고 있는지 알 수 있을까요? 어떻게 사용자는 마케팅에서 주장하는 것이 적절하다는 것을 알 수 있을까요? 만일 제안된 프로토콜이 그런 주장들을 절대 달성할 수 없다면 어떻게 될까요?
IOHK가 Cardano를 만들기를 원했던 가장 큰 이유 중 하나는 프로세스에 대한 합의와 존중이 결여되어 있기 때문입니다. 우리는 더 효과적이고 정상적이며 정직하게 일하는 예시로서 사용될 수 있는 리퍼런스 프로젝트를 개발하고자 했습니다.
우리의 목표는 완전히 새로운 개발방법론과 프로토콜을 제안하는 것이 아닙니다. 오히려 위대한 소프트웨어와 프로토콜이 이미 존재함을 인지하고, 그러한 생성을 유도한 환경을 모방하는데 있습니다. 둘째로는 이 조건들을 공개적으로 알리고 공익을 위해 모방될 수 있는 오픈 소스를 만드는 것입니다.
사실과 의견들
다른 관심사는 사실이 끝나고 의견이 시작되는 지점에서 나옵니다. 수백 가지 프로그래밍 언어, 수십 가지 개발 패러다임, 그리고 프로젝트 관리에 대한 하나 이상의 철학이 있습니다. 학문적 세계에는 비즈니스 관심사부터 실용성에 이르는 영역에서 가지를 뻗은 자체 도전 과제로 가득합니다.
우리는 카르다노 프로젝트에서 보편적으로 인정되고, 공학적 관점에서 유용할 수 있는 확실한 결함을 포착하고자 했습니다. 예를 들어, 암호화 및 분산 시스템은 무심코 끔찍한 실수를 저지를 수 있는 방법에 관한 사례가 너무도 많은, 놀랄만큼 얽혀 있는 주제입니다. 그러므로, 이런 도메인에 관한 통찰력을 필요로 하는 모든 프로토콜들은 인정된 전문가에 의해 설계되어야 하고, 다른 전문가들에게 검증받도록 제출되어야 합니다.
우로보로스는 이 영역에서 첫 번째 사례 연구입니다. 우로보로스는 크고 다양하며 공개적으로 검증 가능한 출판 이력을 가지고 있는 암호학자 팀에 의해 설계되었습니다. 우로보로스는 적대적 모델과 증명, 보안 가정 그리고 표준 암호화 프로세스에 따라 설계되었습니다.이 증명들은 학회의 제출20 그리고 캠브리지 대학의 팀21 이 작성한 독립적인 컴퓨터 증명을 통해 확인되어졌습니다.
그러나 이러한 작업들이 유용성을 보장해 주진 못합니다 – 단지 몇가지 가정들에 대한 보안 모델을 엄격히 체크한 것입니다. 유용성을 위해선, 실제로 프로토콜을 구현하고 테스트하는 것이 필요합니다. 우리 개발자들은 하스켈과 러스트에서 모두 구현하고 테스트하였습니다. 이 작업은 우리가 Ouroboros Praos의 생성으로 이어지는 동기화 모델에 집중해야 할 필요가 있음을 보여주었습니다.
반복의 기술이란, 각각의 단계에서 새로운 교훈과, 이전 스텝22 의 정확성을 재검증하기 위한 요구사항을 얻어내어 위대한 프로토콜을 만들어 내는 것입니다. 이러한 반복은 비용이 많이 들고, 시간이 많이 걸리고, 때로는 참으로 지루한 일이지만, 프로토콜이 정확하게 설계되었다는 것을 보장하기 위해 필요합니다.
프로토콜은 – 특히 수십억의 사람들에게 사용되어지는 – 쉬이 사라지지 않고, 빠르게 진화합니다. 오히려 수 년에서 수십 년동안 프로토콜을 따라야 합니다. 우리 모두가 앞으로 다음 100년을 함께 할 새로운 금융 시스템을 세상에 짐 지우기 전에, 시스템의 디자이너에게 엄격함과 지루함을 요구하는 것은 지극히 당연한 것입니다.
기능상의 죄
더 주관적인 영역으로 들어간다면, 소프트웨어 개발에서 쓰이는 도구, 언어 그리고 방법론들은 사실 객관적인 진실이라기 보다는 종교적 섭리의 산물입니다. 소스코드들은 마치 산문과 같습니다. 모든 사람들은 각자 무엇이 선한가에 대한 의견을 가지고 있습니다. 그리고 종종 전달하고자 하는 내용은 전달하는 방법보다 덜 중요해집니다.
최소한 누군가의 눈에는 잘못된 것으로 보일 것이라는 것을 인정하지만, 우리는 어느 한 쪽을 선택하는 죄를 범해야만 합니다. 하지만 우리의 선택에는 적어도 정당화할 수 있는 많은 근거들이 있습니다.
카르다노를 가능하게 하는 프로토콜은 하스켈로 구현되고 있습니다. 유저 인터페이스는 Daedalus라는 Electron의 포크로 캡슐화 되어 있습니다. 우리는 가능하다면 웹 아키텍쳐 모델을 사용하기로 하였으며, 데이터베이스로는 RocksDB를 활용한 key-value 패러다임을 선택했습니다.
컴포넌트 레벨에서 이 추상화는 유지보수를 더 쉽게하고, 추후 쉽게 더 나은 기술로 교체할 수 있으며, 그리고 우리의 기술 스택이 Github과 Facebook의 개발 노력과 부분적으로 연관되어 있음을 의미합니다.
WebGul을 사용함으로써, 수십만의 자바스크립트 개발자들이 활용하는 도구를 가지고 프론트엔드 기능 개발에 React를 활용할 수 있습니다. 웹 아키텍쳐를 사용한다는 것은 각 컴포넌트들이 서비스로 여겨질 수 있고, 보안 모델이 합리적인 것을 의미합니다.
프로토콜 개발에 하스켈을 선택하기로 한 것은 가장 어려운 결정이였습니다. 함수형 세계에서도 여러가지 다양한 선택이 있었습니다. 좀 더 융통성있고 혼합적인 측면에서는, Clojure, Scala, F#과 같은 언어가 있습니다. 이 언어들은 자바와 .Net의 생태계의 거대한 라이브러리의 혜택을 누리면서, 몇몇 부분에서 함수 프로그래밍의 최상의 면을 유지합니다.
Agda와 Idris와 같은 학문 지향 언어는 정확성을 강력하게 검증 할 수 있는 기술과 관련이 있습니다. 그러나 이 언어들은 괜찮은 라이브러리가 부족하고 개발 경험이 적습니다.
카르다노는 Ocaml과 Haskell을 선택했습니다. Ocaml은 훌륭한 공동체, 훌륭한 도구, 충분한 개발 경험 및 Coq23 를 통한 공식적인 검증 영역에서 훌륭한 유산을 가진 멋진 언어입니다. 그렇다면 왜 우리는 하스켈을 선택했을까요?
왜 하스켈인가?
카르다노를 구성하는 프로토콜들은 분산되어져 있고, 암호화되어 제공됩니다. 그리고 매우 높은 수준의 오류 내구성을 요구합니다. 최선의 상황에서도, 여전히 Byzantine actors는 만연할 것이고, 잘못된 메시지와 클라이언트의 실수로 의도치 않은 유해를 네트워크에 끼칠 것 입니다.
첫째로, 우리는 쉽게 Quickcheck같은 도구를 사용할 수 있는 강한 타입 시스템과 그리고 Refinement Types 같은 정교한 테크닉을 사용하면서도 충분한 내결함성을 가진 언어를 원했습니다. Erlang 스타일의 OTP 모델은 후자를 만족 시키지만 Haskell이나 Ocaml 같은 언어는 전자를 만족시킵니다.
Cloud Haskell이 출시되고, 하스켈은 Erlang의 많은 장점들을 얻었고, 스스로의 정체성을 잃지 않았습니다. 게다가, 하스켈의 모듈성과 조합성을 통해 타임 워프라는 가벼운 맞춤형 라이브러리를 카르다노를 위해 사용할 수 있습니다.
둘째로, 하스켈 라이브러리들은 지난 몇년간 Galois, FP Complete 그리고 Well-Typed 같은 기업들의 광범위한 작업 덕분에 크게 진화했습니다. 그 결과, 하스켈은 상용 어플리케이션 작성24 을 위한 언어로 사용될 수 있게 되었습니다.
셋째로, PureScript의 급격한 진화는 Clojurescript가 Clojure에게 끼친 것과 유사한 연결점을 JavaScript 진영에 제공하였습니다.우리는 카르다노가 브라우저에서 작동하고, 모바일 지갑을 개발하는데 있어서 PureScript는 매우 중요한 역할을 할 것으로 기대합니다.
넷째로, 하스켈은 의존성 해결과 관련하여 지난 몇 년 동안 상당한 사회적, 기술적 노력을 기울였습니다. 그것은 Michael Snoyman과 같은 기술자들이 사용하기에 편리하고 FP Complete가 잘 지원하는 stackage라는 플랫폼을 통해 주도되었습니다.
다섯째, 적절한 의존성 해결을 넘어 우리는 소프트웨어 빌드를 재현할 수 있는 것을 목표로 합니다. 바꾸어 말하면 동일한 구성 값과 종속성 버전을 사용하면 똑같은 빌드 결과물을 생성해야 합니다. 우리는 stackage를 통해 NixOps를 사용하여 소프트웨어 빌드 재현을 성공적으로 달성했습니다.
마지막으로, 하스켈 전문의 개발자 인재 풀은 다른 언어들과 비교했을 때 충분히 컸고, 학문적으로나 현업에서나 적절하게 결합된 인증과 훈련을 받았습니다. 그리고 경험 있는 하스켈 개발자인데 컴퓨터 공학에 대해 세부적인 지식이 없는 경우는 드물기 때문에, 하나의 역량 필터로서 작용하였습니다.
공식 사양과 검증
입증된 올바른 보안 모델을 사용하여 프로토콜을 개발하는 것의 중요한 강점은 적대적인 영향력이 제한되도록 보장한다는 것입니다. 프로토콜을 준수하고 증명이 정확하다면, 적대적 세력은 보안 속성을 위반할 수 없는 계약을 부여받습니다.
깊은 숙고는 이전 주장을 더 중요하게 만들어 줍니다. 적대세력은 얼마든지 지능적이고 유능할 수 있습니다. 그들을 단지 수학적인 모델을 통해 격퇴했다고 말하는 것도 대단합니다. 물론 그것이 모두 사실은 아니지만요.
현실에서는 순수한 보안과 올바른 행동이 존재할 수 없게 하는 많은 요인들과 환경들이 있습니다. 구현은 잘못될 수 있습니다. 하드웨어는 이전에는 고려하지 못했던 공격 방식이 나타나게 할 수 있습니다. 보안 모델이 미흡하여 실제에 적용하기 부적합할 수 있습니다.
프로토콜에 얼마나 많은 사양, 엄격함, 검사가 요구되는지 권위있는 판단이 필요합니다. 예를 들어, 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을 점진적으로 추가할 것입니다.
마지막으로, 공식 검증은 그 검증의 기반이 되는 규격과 사용 가능한 도구들 만큼만 의미 있습니다. 하스켈을 선택하는 주된 이유 중 하나는 그것이 실재와 이론의 올바른 균형을 제공한다는 것입니다. 백서에서 파생된 명세는 하스켈 코드와 매우 흡사하고 두 가지를 연결하는 것은 명령형 언어를 사용하는 것보다 훨씬 쉽습니다.
적절한 명세를 파악하고 업그레이드, 버그 픽스 등 여러 변화가 생길 때 명세를 업데이트하는 것은 여전히 어려운 점이 많습니다. 하지만 이러한 현실이 전체적인 가치를 훼손하지는 않습니다. 입증 가능한 보안에 관해 기초를 구축하려 한다면, 그 구현은 실제로 논문에 제안된 것이어야 합니다.
투명성
암호통화개발의 과학과 공학을 논의할 때 마지막 질문은 어떻게 투명성을 다룰 것인가 하는 점입니다. 설계 결정은 예/아니오로 결정될 수 있는 것이 아니고, 꿈속에서 개발자에게 다가와 갑자기 실제로 일어나는 천상의 무언가가 아닙니다. 그것들은 이전의 실수에서 배운 경험, 토론 및 교훈에서 도출되는 것입니다.
어려운 점은 완전히 투명한 개발 프로세스는 토론이 근거에 기반하기 보다는 보여주기 식으로 흐르도록 영향을 미칠 수 있다는 것입니다. 커뮤니티를 꺾고 이기려는, 그리고 멍청하게 보이는 것에 대한 두려움과 같은 자아들은 대화를 황량하고 비생산적으로 몰아가게 됩니다.
게다가, 외부세력은 그들의 특정 방향의 주제가 유일한 토픽이 될 수 있도록 대화의 주도권을 잡으려고 할 수 있습니다. 모든 사람에게 신성불가침 영역이 있습니다.
그렇다면 핵심 개발자들에게 진전을 위임하는 공동체에서 차용한 투명한 개발 프로세스에 대한 필요성과, 두려움 없이 표현할 수 있는 자유에 대한 필요성 사이에서 어떻게 균형을 유지할 수 있을까요?
카르다노는 감독 기관을 통한 표준기반절차를 받아들이기로 하였습니다. 커뮤니티는 이론과 코드가 잘 검토되는지, 개발자들이 제안한 것들이 실제로 해결되는 지를 알아야 합니다. 이 목적을 위해 peer review는 반드시 과학적 구성요소를 완전히 만족시켜야 합니다. 과학적 구성요소란 바로 상기의 목적을 위해 디자인 된 것이며, 우리에게 현대적인 세상을 가져다 주었습니다.
코딩에 있어서, 이 주제는 좀 더 주관적입니다. 카르다노 프로젝트에서는 IOHK의 작업의 최종 감사인으로 카르다노재단을 선출했습니다. 그들은 특히 다음과 같은 의무를 맡게 될 것 입니다.
- 카르다노 Github에 보관된 소스에 대해 정기적으로 리뷰하고, 품질, 테스트 커버리지, 커멘트의 적절성과 완결성을 검사합니다.
- 모든 카르다노 문서에 대한 정확성과 유용성을 평가합니다.
- 과학자들에 의해 만들어진 프로토콜이 온전히 구현되었는지 확인합니다.
이 임무를 수행하기 위해 IOHK는 정기적인 보고서를 재단에 제출하고, 재단 또는 재단이 임명한 자는 이를 평가합니다. 재단은 최소한 분기마다 카르다노 커뮤니티를 위해 개발 감독 보고서를 발표할 것입니다.
이 첫번째 노력은 탈중앙 프로젝트가 어떻게 책임을 수행할 지에 대해 보다 폭넓은 대화를 이루기 위한 것입니다. 신뢰할 수있는 제 3자의 개발 감독은 개발자들이 궤도에 진입하는 것을 보장하는 강력한 도구이지만 프로젝트가 항상 결과물을 내는 것을 보장하기에 충분하지 않습니다.
이런 이유로, 재무 시스템이 CSL에 병합된 후, 재단은 추가적인 개발팀이 IOHK와 함께 다른 클라이언트를 정식 명세에 맞춰 개발할 수 있도록 장려할 것입니다. 개발 다양성은 단일 아이디어 또는 개발자를 중심으로 단일 문화를 형성하는 것을 피하기 위해 Ethereum 프로젝트에서 사용되는 훌륭한 기법입니다.
명세와 관련해서는 WC3 및 IETF가 따르는 표준 프로세스에서 풍부한 지식을 얻을 수 있습니다. 궁극적으로 카르다노가 통합하고 있는 각각의 프로토콜은 학술적인 연구나 소스코드에 독립적인 사양을 필요로 합니다. 오히려 RFC와 같은 형식이 적합합니다.
카르다노재단의 핵심 원칙 중 하나는 Cardano 프로토콜을 위한 표준 기구로서 역할을 하며, Cardano와 관련된 표준을 업데이트, 추가 또는 변경하기 위한 대화를 주관하는 것입니다. 만일 표준들의 산물인 인터넷이 IETF를 통해 어떤 코어 프로토콜이 사용되어야 할 것인지에 대한 합의에 도달할 수 있다면, 전담 조직도 동일한 결과를 촉진 할 수 있다고 가정하는 것이 전적으로 합리적입니다.
마무리 지으면서, 블록체인 위에서 호스팅 되는 탈중앙화 된 객체로 논점을 옮기는 것도 흥미로울 것입니다. 이 개념은 분산자치기구(DAO)라 불리며 예비 작업들이 이 분야에서 진행중에 있습니다. 필요하다면 IOHK는 카르다노와 통신하는 객체들을 위한 DAO 참조 모델을 개발할 것이며, 카르다노재단은 그들의 표준 절차에 따라 채택 여부를 결정할 권리를 가지고 있습니다.
18: 시가 총액 별 종합 리스팅은 www.coinmarketcap.com을 참조하십시오.
19: 이더리움은 옐로 페이퍼 (Yellow Paper)라고 알려진 준 공식적인 명세를 가지고 있습니다. 하지만 EVM 의미론은 완전히 명세되지 않았거나 프로토콜의 전체 구현에 충분하지 않습니다.
20: IACR’s Annual Crypto Conference in California 의 승인된 논문 71
21: Professor Lawrence Paulson 지도 , Kawin Worrasangasilpa 작성
22: 흥미로 접선을 따라가 보려는 분은 Halmos 교수의 discussion about how to write a math textbook을 보십시오.
23: 이 시점에 더해서, IOHK는 사실 우리가 익명의 Bill White로부터 물려받은 Qeditas라고 불리는 Ocaml에서 구현 된 프로젝트를 가지고 있습니다.
24: 브라이언 오 설리반 (Bryan O’Sullivan)의 하스켈의 산업용 사용에 대한 긍정적 의견입니다.
You must log in to post a comment.