고위험 코드의 버그를 제거하기 위한 방법으로, 형식 검증이라는 소프트웨어 프로그래밍 스타일이 블록체인 세계에 도입되고 있습니다.
간단히 말해, 형식 검증은 수학을 사용하여 프로그램의 논리를 명시하고 오류를 분석합니다. 그러나 시간과 비용이 소요되기 때문에 형식 검증은 인간의 생명이나 큰 금액이 걸린 상황에서 가장 적합합니다.
현재 형식 검증은 교통, 군사 및 암호학에서 고위험 코드의 정확성을 검증하는 데 사용됩니다. 칩 회사들은 이를 사용하여 알고리즘을 강화한 후 실리콘에 임베드합니다. 그리고 은행들은 이를 사용하여 금융 알고리즘을 개발합니다.
블록체인 기술에 적용되면, 형식 검증은 스마트 계약으로 알려진 자동 실행 거래가 의도한 대로 작동할 것이라는 보장을 제공하여 코딩 오류로 인한 일부 버그와 재정적 손실을 제거할 수 있습니다.
올해만 해도 이더리움의 파리티 지갑에서 발생한 버그로 인해 1억 8천만 달러의 손실이 발생했습니다. 작년에는 DAO라는 가상 조직의 버그로 해커가 이더리움 스마트 계약에서 5천만 달러를 빼내는 사건이 발생했습니다.
카르다노와 테조스와 같은 플랫폼은 이미 형식 검증을 용이하게 하기 위해 특별히 설계된 스마트 계약 언어를 개발하고 있습니다. 이더리움 또한 스마트 계약에 형식 검증을 도입하기 위해 노력하고 있습니다.
하지만 형식 검증이란 무엇일까요? 어떻게 작동하나요? 그리고 소프트웨어를 처음부터 제대로 만드는 것이 왜 이렇게 어려울까요?
인간은 실수를 한다
소프트웨어는 본질적으로 용서가 없습니다. 건물을 짓는 경우, 못이나 나사를 빼먹어도 구조물은 여전히 서 있을 수 있습니다. 그러나 소프트웨어의 경우, 단순한 오타 하나가 전체 프로그램이 작동하지 않게 만들 수 있습니다.
“프로그래밍 언어는 믿을 수 없을 만큼 강력합니다,”라고 NASA의 전 수석 과학자인 제라드 홀츠만이 Bitcoin Magazine과의 인터뷰에서 설명했습니다. “프로그래머로서 많은 세부 사항을 다뤄야 하며, 모든 세부 사항을 정확히 맞추지 않으면 어떤 영향이 있을 수 있습니다.”
소프트웨어를 올바르게 만드는 전통적인 접근 방식은 테스트입니다. 알고리즘을 작성한 후, 변수를 입력하고 올바른 출력을 반환하는지 확인합니다. 하지만 모든 입력을 어떻게 테스트할 수 있을까요? 불가능합니다. 테스트할 것이 너무 많고, 테스트하지 않은 경우에 오류가 숨어 있을 수 있습니다.
“가능한 실행이 너무 많기 때문에, 실제로 테스트하거나 실행할 때는 가능한 것의 표면만 긁는 것입니다,”라고 홀츠만이 말했습니다.
다시 말해, 테스트는 버그의 존재만을 찾고 버그의 부재를 찾지 않으며, 작은 실수 하나가 치명적인 결과를 초래할 수 있습니다.
“후쿠시마와 쓰리 마일 섬과 같은 시스템의 실패를 살펴보고 그 실패로 이어진 사건의 순서를 보면, 특정 상황에서 발생할 것이라고 아무도 예측할 수 없었던 많은 것들이 항상 흥미롭습니다,”라고 홀츠만이 말했습니다. “소프트웨어에서도 마찬가지입니다; 많은 일이 발생할 수 있습니다.”
대조적으로, 형식 검증은 한 번에 하나의 상황을 테스트하는 대신 프로그램이 모든 상황에서 작동하는지 테스트하는 방법입니다. 당신이 신경 쓰는 것은 논리가 참인지 여부이며, 그 논리를 확인하는 가장 좋은 방법은 컴퓨터입니다.
“형식화는 당신이 사물에 대해 추론할 수 있도록 하는 목적이 있으며, 사물에 대해 추론하는 가장 유용한 방법은 기계를 프로그래밍하여 당신을 대신해 추론하게 하는 것입니다,”라고 홀츠만이 말했습니다.
계획 세우기
일반적으로 형식 검증의 첫 번째 단계는 수학적 모델을 만드는 것입니다. 필요한 수학은 복잡하지 않으며, 기계가 검사할 수 있는 이른바 “형식 언어”로 작성된 기본 논리입니다.
일반적으로 모델을 명시하는 과정은 시스템이 수행해야 할 작업을 이해하는 이해관계자와 함께 시작됩니다. 의료 기기의 경우, 이해관계자는 의사일 수 있으며, 스마트 계약의 경우 변호사나 은행가일 수 있습니다.
이해관계자의 역할은 자신의 머릿속 정보를 요구 사항 엔지니어에게 전달하여 그 정보를 수집하고 모델을 만드는 것입니다. 이 과정은 비공식적인 논의와 추상화로 시작되지만, 정밀한 수학적 명세로 공식적으로 끝납니다.
이것은 쉽지 않습니다. 상황에 따라 몇 달이 걸릴 수 있는 시간 소모적이고 반복적인 과정이지만, 프로그래머가 소프트웨어의 동작에 대해 깊이 생각하도록 강제하기 때문에 이전에는 없었던 명확성을 가져옵니다.
“이것을 법과 규정으로 생각할 수 있습니다,”라고 독일 자르란트 대학교의 소프트웨어 공학 교수인 안드레아스 젤러가 형식 명세를 건물 계획을 개발하는 것에 비유했습니다.
“당신은 규정을 다듬습니다,”라고 그는 Bitcoin Magazine에 말했습니다. “하지만 처음부터 규정이 없다면, 당신의 건물은 무너지고, 그때 당신은 계획을 세워야 한다는 것을 깨닫게 됩니다.”
논리 검증
모델이 명시되면, 다음 단계는 증명을 통해 모델의 논리를 검증하는 것입니다. 이는 과정에서 중요한 단계입니다. “증명이 없다면, 모델이 현재 상태로 작동할 것이라는 보장이 없습니다,”라고 젤러가 설명했습니다.
그러나 모든 논리적 단계를 명시해야 하기 때문에 증명은 매우 길고 복잡할 수 있습니다. 과거에는 이것이 형식 검증을 고통스럽게 어렵게 만들었습니다. 가장 간단한 진술조차도 수십 개의 정리와 보조 정리를 필요로 할 수 있습니다.
다행히도 요즘 많은 형식 시스템은 Coq, Isabelle 또는 Metamath와 같은 자동 정리 증명기를 사용하여 형식 증명을 검사하거나 심지어 부분적으로 구성할 수 있습니다.
모델이 작동하는 것으로 증명되면, 다음 단계는 프로그램을 구축하는 것입니다. 그러나 여전히 구축한 소프트웨어가 명세에 부합하는지 확인해야 합니다.
이때 ML, Haskell, OCaml 또는 F#와 같은 함수형 프로그래밍 언어가 등장합니다. 이러한 언어는 표현력이 대수에 더 가깝기 때문에 C, Java 또는 JavaScript와 같은 언어보다 형식 검증에 더 적합합니다.
이러한 이유로, 테조스는 OCaml로 작성되었고 카르다노는 Haskell로 작성되어 프로토콜 변경 사항을 형식적으로 검증하기가 더 쉽습니다. (카르다노의 합의 알고리즘을 지원하는 차세대 Ouroboros Praos에 대한 형식 명세도 이미 진행 중입니다.) 마찬가지로, 테조스의 스마트 계약 언어인 미켈슨은 OCaml을 기반으로 하고 있으며, 카르다노의 스마트 계약 언어인 플루투스는 Haskell을 기반으로 하고 있습니다.
장단점
장점으로는 형식 검증이 컴퓨터 과학자들에게 소프트웨어 개발에 대한 더 큰 확신을 제공합니다. 단점으로는 엄격함 때문에 형식 방법이 코드를 개발하는 프로젝트에 시간 소모적이고 비용이 많이 드는 작업이 될 수 있습니다.
이 때문에 형식 방법은 반복적으로 재사용되는 작은 코드 블록을 보장하는 데 가장 적합합니다. 예를 들어, 전체 운영 체제에는 사용하지 않지만, 가장 높은 안전성이나 보안 보장이 필요한 시스템의 일부에만 사용해야 합니다.
자연스럽게도 모든 종류의 보안은 비용이 듭니다. 질문은 블록체인 및 스마트 계약 개발자들이 얼마나 많은 보안을 위해 기꺼이 비용을 지불할 것인가입니다.
오류 없는 것을 원한다면, “완전한 증명을 제공할 사람들에게 수만에서 수십만 달러를 지출할 준비를 해야 합니다,”라고 젤러가 경고했습니다.
반면, 수천만 달러의 자금을 확보하는 스마트 계약의 경우, 이러한 비용은 충분히 가치가 있을 수 있습니다. 다른 관점에서 보면, 경쟁 환경에서 형식 검증은 소비자에게 스마트 계약을 더 매력적으로 만들 수 있습니다.
예를 들어, 형식 검증을 받은 스마트 계약에 자금을 맡기는 것과 받지 않은 스마트 계약 중에서 선택할 수 있다면, 어떤 것을 선택하시겠습니까?
