정식검증(Formal Verification) 방식은 도입 초기부터 '틈새, 비인기' 등의 단어로 연결됐다. 일각에서는 정식 검증 방식이 '군사급' 해킹 방지 방식이라는 말도 있어 이 기술에 미스터리를 더했다.
정식 검증 방법이란 정확히 무엇입니까?
Wikipedia는 공식 검증을 다음과 같이 설명합니다.
컴퓨터 하드웨어(특히 집적 회로) 및 소프트웨어 시스템의 설계 프로세스에서 형식 검증의 의미는 수학적 방법을 사용하여 하나 이상의 형식 사양 또는 속성에 따라 정확성 또는 부정확성을 증명하는 것입니다.
신비감은 아마도 정의에 있는 두 개의 엄격하고 추상적인 키워드인 "공식 사양"과 "수학적 방법 증명"에서 비롯되었을 것입니다. 사실, 이 수수께끼의 층을 밝혀내면 공식 검증의 많은 흥미로운 측면을 발견하게 될 것입니다.
다음 기사에서 논의하고 싶은 질문은 다음과 같습니다. 이 단계에서 형식 검증에 대한 귀하의 상상력을 만족시킬 수 있는 이야기는 무엇입니까? 블록체인 공간에서 공식 검증이 정말 기술로 자리잡을 수 있을까요? 그렇다면 어떻게 할 수 있습니까?
(PS: 위에서 언급한 "공식 명세"의 개념도 아래에서 논의될 것입니다.)
위의 질문에 답하기 위해 먼저 다른 간단한 질문을 고려할 수 있습니다.
>이 단계에서 사람들은 무엇을 위해 형식적인 방법을 사용합니까?
이 질문에 대한 답변은 두 가지뿐입니다.
>1. 실수를 피하라
>첫 번째 레벨 제목
| 실수를 피하십시오
실수를 피하는 것은 실제로 손실을 피하는 것입니다.
프로그래밍 오류에 대해 절대 허용되지 않는 영역이 무엇인지 먼저 살펴보겠습니다. 프로그래밍 오류로 인한 손실이 측정 불가능한 영역은 어디입니까?
사실 형식적인 방법은 하드웨어 설계 이후 대중화되었습니다. 유명한 예는 다음과 같습니다. Intel의 Pentium CPU 부동 소수점 장치에 오류(FDIV 버그)가 발생하여 수만 개의 CPU를 재활용하고 교체해야 했으며, 이로 인해 Intel에 막대한 손실이 발생했습니다(4억 7500만 달러)[1].
그 이후로 인텔은 칩 설계에 형식적인 방법을 광범위하게 채택했습니다.
IBM, AMD, NVIDIA 및 CADENCE[2]와 같은 컴퓨터 하드웨어 거대 기업도 형식적 방법의 사용자입니다...
도랑을 통해 많은 지혜를 배울 수 있다는 말은 사실 각계각층에 시행착오를 겪는 사람들이 있고, 산업계도 마찬가지다. 예를 들어, 1996년 유럽 우주국의 아리안 5호(Ariane 5) 로켓의 첫 발사는 관성 항법 시스템에서 보낸 잘못된 명령(부동 소수점 숫자를 정수로 변환하여 오버플로 발생)으로 인해 로켓이 겨우 발사되었습니다. 37초 동안, 그리고는 정해진 궤적을 벗어나 결국 추락했다. 유럽 우주국의 막대한 연구 개발 자금(80억 달러)[3]이 화염에 휩싸였습니다.
그로부터 얼마 지나지 않아 EADS는 공식 방법을 사용하여 Ariane 로켓의 임무 일정 모델을 개발하기 시작했습니다.
미국항공우주국(NASA)과 영국 국방부는 1990년대 [4]에서 연속적으로 설계 표준을 발표했으며, 그 중 형식적인 방법의 사용이 나열되었습니다. 우리나라의 Yutu 달 탐사선 제어 시스템과 우리나라 최초의 자체 개발 우주선 내장형 실시간 운영 체제 SpaceOS[5]도 정식 방법을 통해 정확성을 검증합니다.
역사의 발전은 돈이 사회 발전을 촉진하는 첫 번째 원동력이라는 것을 말해줍니다! 아무도 프로그램 오류로 인한 막대한 손실을 한숨 돌릴 여유가 없습니다.
위의 두 가지 이야기가 너무 무겁게 들린다면 다음 그림을 살펴보자.
위의 그림은 공식적인 방법을 사용하여 개발된 메트로 프로젝트의 글로벌 분포를 보여줍니다[6].
파리지하철 신호시스템을 시작으로 북미, 유럽, 아시아, 남미 일부 국가의 지하철 시스템 개발에 형식적인 방법이 널리 사용되고 있음을 알 수 있다. 이것이 아마도 우리가 지하철 시스템 고장으로 인한 큰 손실과 재해에 대해 거의 듣지 못하는 이유일 것입니다.
다시 말하지만, 돈은 주요 생산력입니다.
일상적인 여행을 보장하는 공식적인 방법의 기여가 널리 인정되었으므로 블록체인 기술을 기반으로 개발된 디지털 자산 분야에서 공식적인 검증 기술을 사용하여 스마트 계약의 보안을 보장하여 재산을 보호할 수 있습니다. 보안이 합리적이고 시급해집니다.
어떻게 해야 하나요? 다음은 간단한 소개입니다.
우선 "공식명세"의 개념을 도입할 필요가 있다.
공식 사양(formal specification)은 시스템의 예상 동작(예: 계정 A에서 계정 B로 다수의 S 토큰 전송) 및 속성(예: 전송으로 인해 계정 B의 오버플로가 발생하지 않음)의 엄격하고 포괄적인 구현을 의미합니다. ) 수학적 언어를 통해 정의. 공식 사양은 종종 시스템의 정확성과 보안을 정의합니다.
시스템의 공식적인 사양이 주어지면 사양에서 시작하여 시스템을 반복적으로 설계하고 구현할 수 있습니다. 반복의 각 단계에서 반복에 의해 생성된 시스템이 정제, 합성 및 형식 증명을 포함한 일련의 방법을 통해 반복 이전의 사양 또는 시스템과 일치하는지 수학적으로 엄격하게 확인할 수 있습니다.
공식 사양에서 시스템을 설계 및 구현하는 것 외에도 기호 실행, 모델 검사 및 공식 증명을 포함한 일련의 방법을 사용하여 기존 설계 및 구현이 이 사양과 일치하는지 확인할 수 있습니다.
웅장하죠?
예를 들어 스마트 계약 프로그램의 경우 각 문의 의미에 따라 가능한 모든 입력(예: 함수 매개 변수의 조합) 및 초기 상태(예: 상태 변수의 초기 값 조합)에서 시작할 수 있습니다. , 문장별로 프로그램의 가능한 모든 종료 상태(예: 계약 실행 후 상태 변수의 값 및 생성된 이벤트 로그)를 추론하고 모든 입력, 초기 상태 및 종료 상태의 조합 여부를 확인합니다. 계약은 공식 사양과 일치합니다. 이것은 Conan이 사건을 단계별로 해결한 방식과 약간 비슷합니다. 그러나 여기에 있는 모든 정의는 엄격한 수학적 언어로 설명되어 있으며 파생 및 검사도 엄격한 수학적 파생 및 증명입니다. 검증할 시스템의 복잡성과 공식 사양에 따라 유도 및 증명을 수동으로 구성하거나 기계에서 자동으로 생성할 수 있습니다.
첫 번째 레벨 제목
| 공격에 대하여
적대적 공격은 실제로 손실을 피하는 또 다른 의미입니다.
이야기는 미군의 전자 공격으로 시작됩니다. 2015년 여름 해커는 미군의 리틀버드 무인헬기를 전자공격하라는 명령을 받고 드론을 장악했다. 그러나 미 국방부가 무인기의 핵심 관제 프로그램을 재개발하면서 해커들은 오늘날 전 세계에 존재하는 모든 공격 방법을 동원했지만 새로 배치된 시스템을 뚫지 못했다[7].
리틀 버드는 어떤 기술로 모든 공격을 막아낼 수 있는 슈퍼 방어 능력을 갖게 될까요? 정답은 공식적인 확인 방법입니다.
정형 검증 방법은 엄격한 수학적 증명을 통해 프로그램 동작이 예상과 일치하는지 확인하지만 정형 검증 프로그램의 정확성은 매우 노동 집약적이므로 프로그램 테스트와 같은 범용 기술과 달리 정형 검증 방법은 보안에만 적용되는 경우가 많습니다. 드론, 우주선, 운영 체제 등에 대한 프로그램 정확성 검증과 같은 중요한 도메인
여기서 언급해야 할 것은 2016년에 발견된 매우 심각한 Linux 운영 체제 커널 취약점인 Dirty Cow(CVE-2016-5195)[8]입니다. 공격자는 이 취약점을 사용하여 시스템의 최고 권한을 얻을 수 있습니다. 시스템이 악용될 수 있습니다.
첫 번째 레벨 제목
| 보안이 중요한 블록체인 분야
블록체인 분야도 마찬가지인데, 한편으로는 작은 실수가 큰 손실로 이어질 수 있고, 다른 한편으로는 막대한 경제적 이익이 많은 공격자를 끌어들일 수 있습니다.
최초의 이더리움 해킹 사건인 The DAO에서 공격자들은 당시 미화 5,500만 달러 상당의 이더리움을 훔쳐 이더리움의 하드포크[11]를 일으켰고, 이후 이더리움 스마트 계약과 관련된 공격이 계속되고 있습니다. , 2017년 11월 이더리움 패리티 지갑이 해킹되어 사용자가 약 1억 5천만 달러 상당의 디지털 자산을 잃게 되었습니다[11].
Ambi Labs의 통계에 따르면 2018년 상반기에만 약 11억 달러의 디지털 자산이 도난당했으며 블록체인 시스템 관련 취약점(예: Ethereum의 스마트 계약 취약점) 및 디지털 자산을 둘러싼 생태계 보안 문제(예: 여러 중앙 집중식 거래소의 절도)가 끝없는 흐름으로 등장하고 있습니다.
현재 블록체인 시스템의 관련 허점과 디지털 자산 생태계의 보안 문제는 궁극적으로 관련 프로그램의 설계 및 구현과 관련이 있습니다. 형식적인 방법 이전에는 이러한 문제가 대부분 프로그램 테스트를 통해 발견되었습니다.
형식 검증이 블록체인 분야에 진입한 초기에 Ethereum 커뮤니티의 Yoichi Hirai는 Ethereum의 스마트 계약 가상 머신 EVM의 완전한 형식 모델링을 수행했습니다. 또한 UIUC University의 팀도 공식적으로 EVM을 모델링하고 검증했습니다[12]. EVM은 이더리움 스마트 계약의 근간을 이루는 핵심으로, 이더리움의 보안과 관련이 있으며 디지털 자산 보호와 같은 주요 이슈를 포함하고 있어 커뮤니티의 광범위한 관심을 받고 있습니다.
또한 MakerDAO 프로젝트는 공식적으로 검증된 최초의 분산 응용 프로그램(DApp)을 출시했습니다[13]. MakerDAO는 스테이블 코인, 담보 대출 및 분산형 커뮤니티 거버넌스 기능을 제공하는 이더리움 기반 스마트 계약 플랫폼입니다. 배포된 스마트 계약의 보안을 보장하기 위해 MakerDAO 팀은 모기지론(CDP)의 핵심 엔진 계약의 계약 코드를 K-Framewok을 통해 확인하여 스마트 계약 프로그램이 해커 공격에 완벽하게 저항할 수 있음을 보여주었습니다.
Ambi Labs는 또한 이더리움 스마트 계약의 공식 검증에 대해 많은 작업을 수행했으며, 스마트 계약을 위한 공식 검증 프레임워크를 제안했으며, 이 프레임워크 내에서 ERC20, ERC721 등과 같은 몇 가지 일반적인 토큰 계약을 증명했습니다(예: 일반 기능 포함). 전송, 토큰 총액 등). 이러한 수학적으로 입증된 스마트 계약은 보안 문제에 대한 걱정 없이 바로 사용할 수 있습니다. 이러한 계약 소스 코드와 증명 프로세스는 오픈 소스의 형태로 커뮤니티에 기여되었습니다[14].
첫 번째 레벨 제목
https://github.com/sec-bit/tokenlibs-with-proofs
|결론
대부분의 사람들은 정형검증 방법이 헤아릴 수 없다고 생각하는데, 그 이유는 정형검증 방법은 일반적인 기술이 아니라 현장과 결합하여 그 가치를 발휘해야 하는 특정 기술이기 때문입니다. 블록체인 분야에서 형식적인 방식이 있으면 좋은 것인지, 꼭 있어야 하는 것인지도 프로젝트의 특성과 불가분의 관계입니다.
블록체인 기술 및 프로젝트 응용 프로그램에 대한 탐색이 계속 심화됨에 따라 실수 방지, 해커 공격 방지 및 재산 손실 방지에 대한 프로젝트 당사자의 요구가 점점 더 강해졌습니다.
첫 번째 레벨 제목
마지막에 작성 | 검증과 테스트 사이의 얽힘에 대해 얼마나 알고 있습니까?
마지막으로 공식 검증과 테스트 간의 관계에 대해 이야기해 보겠습니다.
"프로그램 테스트는 오류가 있음을 증명할 수 있지만 오류가 없음을 증명할 수는 없습니다." Edsger Dijkstra(1972년 튜링상 수상자이자 형식적 방법의 핵심 아이디어 제안자)는 이렇게 논평했다.
실제로, 특히 코드가 충분히 복잡한 시나리오에서 형식 검증(Verification)과 프로그램 테스트 방법(Testing)의 검증 효과는 구름과 진흙처럼 다릅니다.
예: 2009년 호주의 과학자들은 산업용 운영 체제의 seL4 마이크로커널의 완전한 기능 검증을 수행하기 위해 형식적 방법을 사용했습니다[15]. 검증 방법은 형식적 검증과 프로그램 테스트의 두 가지 방법으로 수행되었습니다. 검증 결과는 다음과 같습니다. 형식적인 방법으로 460개 이상의 버그가 발견되었지만 프로그램 테스트에서는 16개의 버그만 발견되었습니다.
더 흥미로운 점은 검증 비용이 높다고 알려진 정식 검증 분야에서 seL4 마이크로커널을 완전 검증하는 검증 비용은 600만 달러에 불과한 반면, 테스트를 통해 CC EAL6 인증을 통과하는 데 드는 비용은 87달러에 달한다는 점이다. 백만 달러[15].
정식 검증을 통해 seL4 마이크로커널에 대한 보다 강력한 보안 보장을 보다 경제적으로 제공할 수 있음을 알 수 있습니다.
참조
참조
【1】History of Formal Verification at Intel
https://dac.com/blog/post/history-formal-verification-intel
[2] Wang Jian: 정식 검증에 대해 이야기해 봅시다.
http://chainb.com/?P=Cont&id=1957
【3】Modeling and Validation of a Software Architecture for the Ariane-5 Launcher
https://link.springer.com/chapter/10.1007/11768869_6
【4】Tenth NASA Formal Methods Symposium
https://shemesh.larc.nasa.gov/NFM2018/
[5] Yutu가 사용하는 국내 SpaceOS 운영 체제는 향후 민간 버전으로 파생될 예정입니다.
http://blog.sina.com.cn/s/blog_ae55841d0101hemg.html
【6】Cimatti, A., Corvino, R., Lazzaro, A., Narasamdya, I., Rizzo, T., Roveri, M., Sanseviero, A. and Tchaltsev, A., 2012, July. Formal verification and validation of ERTMS industrial railway train spacing system. In International Conference on Computer Aided Verification (pp. 378-393). Springer, Berlin, Heidelberg.
【7】COMPUTER SCIENTISTS CLOSE IN ON PERFECT, HACK-PROOF CODE https://www.wired.com/2016/09/computer-scientists-close-perfect-hack-proof-code/
[8] Dirty Cow를 사용하여 도커 탈출 실현
https://www.anquanke.com/post/id/84866
【9】CertiKOS: Yale develops world’s first hacker-resistant operating system
https://www.ibtimes.co.uk/certikos-yale-develops-worlds-first-hacker-resistant-operating-system-1591712
【10】Fengwei Xu, Ming Fu, Xinyu Feng, Xiaoran Zhang, Hui Zhang and Zhaohui Li. A Practical Verification Framework for Preemptive OS Kernels. Proc. 28th International Conference on Computer Aided Verification (CAV’16)
【11】THE DAO에 대한 기술적 관점의 공격 방법 분석
https://www.8btc.com/article/93713
【12】kframework/evm-semantics
https://github.com/kframework/evm-semantics
【13】벤처 캐피털 거인 A16Z, 스테이블 통화 프로젝트 MakerDAO에 투자
https://www.jinse.com/bitcoin/246582.html
[14] 스마트 컨트랙트 보안 문제를 해결하기 위한 공식 증명 구성 - 계약이 시급히 증명되어야 합니다.
https://mp.weixin.qq.com/s/xUNKT8v9ikEYFnuMWzvXdg
【15】Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. 2009. seL4: formal verification of an OS kernel. In Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles (SOSP '09).
IOS
Android