지능 계약 빈틈, 사슬의 아카류스 발뒤꿈치

	     ，            ，          ，       。                   ：     3.4                     。

지능 계약의 빈틈, 공체인이 감출 수 없는 칸막이 이태방의 지능 계약에 빈틈이 있다는 것은 이미 뉴스가 아니다.이른바 스마트 계약이란 사실 일련의 코드인데 이 일련의 코드는 다른 소프트웨어 코드와 현저한 차이가 없다.다만 이 코드들은 돈과 관련이 있는 경우가 많기 때문에 이 코드에 빈틈이 생기면 공격을 당하면 막대한 손실이 발생할 수 있다.더DAO는 2016년 5월 귀속호출 이더리움을 이용해 빈틈을 보내는 해커의 공격을 받아 큰 피해를 봤다.2017년 7월 19일 패리티 월렛의 다중서명 지갑('멀티-sig') 코드에 있는 허점이 해커에 이용되면서 ETH의 거액 잔액을 보유한 지갑 계좌 3개가 해킹됐다.2018년 4월 22일 BEC 스마트계약 대량이체 함수 중 한 줄의 코드에 버그가 있어 빈틈이 생겼다.해커들은 이 구멍을 이용해 아메리칸 체인의 스마트 계약을 공격해 수억에 달하는 엄청난 양의 BEC token을 생성하고 돌리는 데 성공했다.2018년 5월에 공격자들은 이더리움 노드의 감권 결함을 이용하여 인터페이스를 악의적으로 호출하여 기호화폐를 훔쳤다. 지속 시간이 2년에 달했고 도난당하고 아직 전출되지 않은 이더리움 화폐의 가치는 현재 가격인 2천만 달러에 달했고 기호화폐의 종류는 164종으로 전체 가치를 가늠하기 어렵다.지능계약의 빈틈으로 공격당한 사례가 처음이 아니라 마지막도 아니라고 믿는 부분만 있다.왜 안전한 블록체인이라고 호칭하는지, 어떻게 해커들 앞에서 이렇게 일격을 가할 수 없는지 의문이 들 수밖에 없다.약속한 가치 인터넷은요?안전성이라고 했는데?
스마트 계약, 보안 빈틈이 큰 문제입니다. 이런 스마트 계약은 제3자 개발자가 만들어낸 빈틈인데 밑바닥 체인과 무슨 관계가 있습니까?이것은 마치 상가와 같다. 상가 위의 상점이 도둑맞았다. 이 상가의 관리자가 말하기를, 너의 상점은 자기 집의 방범문이 좋지 않은데, 내 상가와 상관없는 일이라고?그러나 만약 상가에서 상인들이 툭하면 도둑질을 하고 도난을 당하는 일이 발생한다면 상인과 사용자가 올까?만약 상점과 사용자가 없다면, 이 상가는 아직 열리지 않겠는가?블록체인의 발전을 보면 블록체인이 비트코인의'코인 투기'특징에서 빼낼 수 있는 이유는'스마트 계약'이 사람들에게 블록체인의 기술 가치와 응용 가치를 보여주기 때문이다.그러나 현재로서는 블록체인의 실제 응용이 보급되지 않았지만 스마트 계약의 빈틈 사건이 먼저 유행하기 시작했다.이런 스마트 계약 때문에 자금과 관련된 경우가 많다.그래서 해커들은 이런 스마트 계약의 빈틈을 찾아 공격을 통해 이익을 얻는 것을 더 좋아한다.스마트 계약의 빈틈이 크게 개선되지 않으면 블록체인의 기술 응용은 완전히 공중 누각이다.아무도 감히 진정으로 가치 있는 물건을 안전 보장이 많지 않은'가치 인터넷'에 놓지 못한다.
스마트 계약의 빈틈, 어떻게 대응해야 하나?사실 스마트 계약의 안전 빈틈이 빈번한 것은 우연이 아니다. 현재 디지털 화폐 시장은 물고기와 용이 섞여 있고 스마트 계약은 효과적인 감독이 부족하며 안전 감사 절차가 부족하다. 그 코드 안전성과 논리적 빈틈은 개발자의 인공 심사만으로 위험과 빈틈이 존재하는 것을 피하기 어렵다.따라서 스마트 계약을 배치하기 전에 이를 전면적으로 깊이 있게 코드 안전 감사를 하고 가능한 한 빈틈을 없애고 위험을 낮춰야 한다.이러한 스마트 계약에 대한 안전 감사에서 형식화 검증은 자주 언급되는 방법이다.형식화 검증이란 어떤 형식화 규범이나 속성에 따라 수학적 방법으로 그 정확성이나 비정확성을 증명하는 것을 말한다.최초로 하드웨어에 보급되기 시작했다.그해 Intel의 Pentium CPU 부동소수점 연산자 오류(FDIV Bug)로 수만 개의 CPU가 회수·교체될 수밖에 없어 Intel에 큰 손실을 입혔다.그 후 Intel은 칩 설계에서 형식화된 방법을 광범위하게 채택하기 시작했다.컴퓨터 하드웨어의 거두인 IBM, AMD, NVIDIA 등도 형식화된 방법의 사용자들이다.우리나라의 옥토끼호 달차 제어시스템과 우리나라 최초로 자체 개발한 우주비행기 삽입식 실시간 운영체제인 스페이스OS도 모두 형식화된 방법을 통해 정확성을 검증했다.
형식화 검증은 어떻게 스마트 계약의 빈틈을 검사하는 데 도움을 줍니까?예를 들어 스마트 계약 프로그램에 대해 우리는 모든 가능한 입력(예를 들어 함수 파라미터의 조합)과 초기 상태(예를 들어 상태 변수의 초기 값의 조합)에서 출발하여 각 문장의 의미에 따라 프로그램의 모든 가능한 종료 상태(예를 들어 계약 집행이 끝난 후의 상태 변수의 값과 발생하는 이벤트 log)를 한 문장씩 유도하고 계약의 모든 입력, 초기 상태,끝 상태의 조합이 모두 형식화 규범과 일치하는지 여부.이것은 코난이 사건을 해결하는 것처럼 한 걸음 한 걸음 추론하는 것과 약간 비슷하다.단지 이곳의 모든 정의는 엄격한 수학 언어 묘사를 통해 이루어지고 유도와 검사도 엄격한 수학 유도와 증명이다.검증을 기다리는 시스템과 그 형식화 규범의 복잡도에 따라 수동으로 구성할 수도 있고 기계가 자동으로 생성할 수도 있음을 유도하고 증명한다.실천에서 유도와 증명이 진행되지 못하는 것은 흔히 설계와 실현에 규범에 부합되지 않는 버그가 존재한다는 것을 의미한다.분석을 통해 케이스의 위치와 원인을 유도하고 증명함으로써 버그가 설계와 실현에서의 구체적인 위치와 원인을 포지셔닝할 수 있다.이런 방법은 디지털 자산 분야에서 엄격한 의미에서 오류를 회피하고 손실을 피하는 것이 가능하다.
형식화 검증은 만능이 아니지만 이런 형식화 검증(Formal Verification)과 프로그램 테스트(Testing)는 별개의 일이다.프로그램 테스트는 오류의 존재를 증명할 수 있지만, 오류가 존재하지 않는다는 것을 증명할 수 없다.예를 들어 2009년에 호주의 과학자들은 형식화된 방법을 사용하여 공업급 운영체제 seL4 마이크로코어에 대해 완전한 기능성 검증을 실시했다. 검증 방식은 형식적인 검증과 프로그램 테스트 두 가지 방식으로 각각 전개되었다. 검증 결과는 형식적인 방법은 모두 460여 개의 버그를 발견했고 프로그램 테스트는 16개의 버그만 발견했다.그러나 주의해야 할 것은 프로그램 테스트는'진실'환경에서 진행되고 형식화 검증은 수학적 차원일 뿐이며'진실'환경에서의 테스트는 형식화 검증으로 대체할 수 없다는 것이다.형식화된 검증을 거쳤다고 해서 스마트 계약에 구멍이 생기지 않는다는 것은 아니다.사람이 만든 코드라면 빈틈이 생길 수 있다.형식화 검증은 개발자만 도울 수 있고 수학적 방법으로 검증할 수 있는 부분을 검증할 수 있을 뿐 검증할 수 없는 부분에 대해서는 형식화 검증도 문제를 해결할 수 없다.그래서 스마트 계약의 안전 문제는 여전히 무겁고 갈 길이 멀다.