9월 5일, Odaily가 주최하고 36Kr Group Strategy가 공동 주최한 POD 컨퍼런스 보안 포럼에서 Cheetah Blockchain Research Center의 보안 전문가인 Yang Wenyu가 "스마트 계약 자동 감사 기술"이라는 제목의 연설을 했습니다.

Yang Wenyu는 스마트 계약 개발 현황을 소개했습니다. 대부분의 사람들은 블록체인이 이제 추운 겨울 기간에 있다고 생각하지만 Cheetah Blockchain Research Center의 통계에 따르면 지난 한 달 동안 새로운 스마트 계약 건수는 하루에 1317건이었습니다. 연구 센터에 포함된 프로젝트 중 블록체인 인프라는 9.38%, 게임 및 VR 4.44%, 커머스 및 소매 3.6%, 소셜 미디어 및 커뮤니케이션 3.4%를 차지합니다.

숫자가 꾸준히 증가하는 동안 스마트 계약도 보안 문제에 직면해 있습니다. 2017년부터 2018년 6월까지 스마트 컨트랙트 취약점이 빈번하게 발생하여 많은 금전적 손실을 입었고 일부 블록체인 개발자나 사용자, 심지어 스마트 컨트랙트까지 스마트 컨트랙트의 보안에 의문을 제기하게 하여 이더리움 이후 이더리움의 발전에도 걸림돌이 되었습니다. 개발.

또한 Fomo3D가 인기를 끌면서 이틀째에만 위조 계약서가 대거 등장했다. 카피캣 Fomo3D 게임 개발사들이 적극적인 유통 논리를 바꿔 투자 자금의 대부분이 카피캣 컨트랙트 개발자들에게 흘러가게 했고, 이는 DApps의 발전에도 걸림돌이 되고 있습니다.

이러한 맥락에서 대규모 스마트 계약의 보안을 효과적으로 보장하는 방법은 무엇입니까? Yang Wenyu는 가장 좋은 방법은 수동 감사의 복잡성을 줄이고 스마트 계약을 사용하여 감사를 자동화하는 것이라고 믿습니다.

특히 자동화된 감사 방법은 세 가지 주요 범주로 나뉩니다.

• 첫 번째는 피쳐 코드 매칭으로 악성코드를 추출 및 추상화하고 매칭 모듈을 구성하여 탐지 대상 소스코드를 탐지하는 것이다. 빠른 속도와 새로운 취약점에 대한 신속한 대응이 장점이지만, 사용 범위가 제한적이고 위음성률이 높다는 단점이 있습니다.
  

• 두 번째는 공식 검증을 기반으로 하는 자동화된 감사 방법입니다. 2016년 Hirai에 의해 처음 제공되었으며 Grishchenko 및 Hildenbrandt에 이어 F* 프레임워크 및 K 프레임워크를 사용하여 EVM을 Formal 모델로 변환하여 개선되었습니다. Formal은 항공우주 분야의 일반적인 형식 검증 프레임워크인 반면 K 프레임워크는 시맨틱 변환 프레임워크입니다.
  

• 마지막 방법은 오늘날 가장 일반적으로 사용되는 방법으로 기호 실행 및 기호 추상화를 기반으로 감사를 자동화합니다. 스마트 컨트랙트를 분석할 때 소스코드를 컴파일하여 EVM OPCODE를 구성한 후 자동 분석 엔진에 입력하여 CFG로 변환한 후 이 두 가지 방법으로 분석할 수 있다. 대표적인 것이 오옌테(Oyente)와 시큐리파이(Securify) 시스템으로 위양성률과 위음성률을 줄일 수 있지만 분석 방법이 번거롭고 시간이 많이 걸린다.
  

그러나 Yang Wenyu는 또한 현재의 자동 감사 방법이 매우 미숙한 단계에 있으며 주로 높은 오경보 비율, 낮은 자동화 수준, 수동 2차 감사에 대한 의존도, 상대적으로 긴 감사 시간이라는 세 가지 주요 문제에 직면해 있다고 지적했습니다.

다음은 Yang Wenyu의 연설 전문입니다. 즐기십시오.

여러분 감사합니다 오늘 이 컨퍼런스에 참석하게 되어 영광입니다 오늘 저의 연설 주제는 현재 스마트 계약 자동화 보안 탐지 기술을 분석하는 것입니다 오늘 저의 연설은 두 부분으로 나눌 수 있습니다. 1부에서는 이더리움의 스마트 컨트랙트 개발 현황을 살펴보고, 2부에서는 이러한 현상을 바탕으로 스마트 컨트랙트 자동화와 관련된 몇 가지 방법을 자세히 설명합니다.

먼저 스마트 컨트랙트 개발 현황을 살펴보겠습니다.저희 플랫폼에 따르면 지난 한 달간 스마트 컨트랙트 건수가 하루 평균 1317건의 증가율로 꾸준히 증가하고 있는 것을 알 수 있습니다. 이는 우리의 이해와 일치할 수 있습니다. 블록체인은 이제 추운 겨울 기간에 있으므로 성장률이 상대적으로 안정적입니다. 둘째, 우리는 일부 NLT 방법을 사용하여 스마트 계약 분야를 구분합니다.일부 민감한 영역을 제외하고 스마트 계약은 이제 인프라, 상업 소매, 게임, 소셜 미디어 및 통신에서 널리 사용됩니다. 이것이 스마트 계약의 현상태입니다. 현재 스마트 계약의 보안 상태는 어떻습니까? 아마도 두 손님이 이미 자세히 설명했을 것입니다. 2017년부터 2018년 6월까지 이러한 스마트 계약 취약점이 자주 발생했습니다. , 매번 많은 양의 재정적 손실을 가져오고 일부 개발자 또는 일부 블록체인 사용자와 스마트 계약조차도 스마트 계약의 보안에 대해 높은 의구심을 갖게 하여 이더리움의 개발을 방해합니다.

또한 방금 게스트가 Fomo3D를 언급한 것도 볼 수 있습니다. 기본적인 스마트 컨트랙트 보안 외에도 현재 보안이 큰 관심을 받고 있습니다. 이런 종류의 게임에서 개발자는 실제로 적극적인 배포 논리를 변경하여 벌집 게임을 플레이하는 과정에서 대부분의 투자 자금이 모방 계약 개발자에게 흘러 갔고 이는 또한 개발에 기여했습니다. DApp.원인 방해.

이제 우리는 대규모 스마트 계약의 보안을 어떻게 효과적으로 보장할 수 있는지에 대한 문제에 직면해 있으며, 이는 오늘 논의할 문제이기도 합니다. 두 번째 부분은 현재 스마트 계약 자동화 감사 기술의 개발을 여러분과 공유하고 싶습니다.

돌이켜보면 어제 낮 12시 기준 이더리움에는 총 193만 건의 스마트 컨트랙트가 있고 일일 증가율은 꾸준히 증가하고 있습니다.현재 감사 방법에는 수동 감사와 자동 감사가 있습니다. 대규모 스마트 계약 중에서 가장 좋은 방법은 자동 감사를 통해 더 많은 작업을 수행할 수 있도록 수동 감사의 복잡성을 줄이는 것입니다. 우리는 자동 감사를 세 부분으로 나눕니다. 먼저 첫 번째 유형은 피처 코드 매칭, 두 번째 유형은 상황 검증 기반의 부차 감사 방식, 마지막 유형은 기호 실행 및 기호 추상화 기반 자동 감사 방식이다.

기능 코드 매칭을 먼저 보세요.악성 코드를 추출하고 추상화한다는 이름에서 명확하게 이해할 수 있습니다.우리는 정적 원본 코드와 일치하는 시맨틱 매칭입니다.감사 방법의 장점은 분명합니다.예를 들어 속도가 매우 빠릅니다. 소스 코드에서 문자열 일치를 수행하면 두 번째가 새로운 취약점을 신속하게 찾을 수 있기 때문에 감사에서 새로운 취약점이 발생하면 새로운 일치 패턴을 신속하게 제출할 수 있습니다. 단점이 무엇인지 다시 살펴보자 현재 블록체인은 개방적이고 투명해야 한다는 점은 이해하지만 실제 상황은 그렇지 않다 통계를 냈을 것이다 현재 코드 개방률은 48.62%에 불과하다 , 즉, 이더리움에서는 컨트랙트의 절반 이상이 오픈소스가 아니고 코드만 노출되어 있고 게스트는 코드를 만드는데도 많은 노력을 기울였다고만 하는데 이러한 제약이 사용범위로 이어집니다. 앱 감지와 같은 기존의 정적 감사 방법은 라이브러리의 일부 고유한 기능을 호출하여 감사합니다.스마트 계약의 일부 기능과 기능은 더 가변적이므로 취약성 비율이 상대적으로 높습니다.

두 번째 방법은 정식 검증을 기반으로 널리 사용되는 자동 감사에 대해 논의하겠습니다.정식 검증 감사 스마트 계약 보안은 2016년 Hirai가 처음 제공했습니다. 코드 논리에 문제가 있는지 판단하고, 이 작업의 마지막 두 작업은 형식적인 측면을 더 개혁하고, Lem 언어를 포기했습니다. 또한 비교적 비효율적인 변환 방법입니다. F* 프레임워크와 K 프레임워크를 사용하여 EVM을 변환합니다. Formal은 항공우주 분야에서 종종 형식 검증을 하는 프레임워크일 수 있으며, K 프레임워크는 시맨틱 변환 프레임워크인 이 두 가지 대표적인 기술 연구를 더 깊이 이해하고 싶다면 참조할 수 있습니다. 다음 논문.

세 번째 요점은 오늘 여러분과 소통하는 데 집중하고 싶은데 가장 일반적으로 사용되는 방법 중 일부는 기호 실행 및 기호 추상화를 기반으로 한 자동 감사입니다. 객체가 무엇인지 먼저 명확하게 분석해야 합니다. 방금 기능 일치 코드에서 설명한 것처럼 EVM에 있는 대부분의 스마트 계약 코드는 공개되지 않았음을 알고 있습니다. 이제 객체를 분석하고 EVM OPCODE여야 함을 확인합니다. 일부 소스 코드를 전달한 후 컴파일하고 자동 분석 엔진에 입력되는 EVM OPCODE를 형성할 수 있습니다. Symbolic Execution과 Symbolic Abstraction을 기반으로 한 이 자동 감사 프레임워크에는 몇 가지 공통적인 특징이 있는데, OPCODE가 엔진에 입력되면 CFG로 변환되어 하나하나 제어 흐름도가 되는 것이다. 이 CFG는 무엇을 의미합니까?CFG는 계약 코드의 논리를 빠른 코드로 패키징하는 것입니다.내부 논리가 분기될 때 왼쪽 계약은 매우 크고 완전한 CFD를 형성하므로 프로그래머가 더 잘 이해하고 실행할 수 있습니다. 약간의 논리.

CFG 생성 후 현재 두 가지 분석 방법이 있습니다. 첫 번째 유형은 기호 실행을 기반으로 한 검증입니다. 이 유형이 더 대표적입니다. 누구나 Mythril, Oyente 및 Maian에 익숙합니다. 공개적으로 사용 가능한 상징적 추상 분석 방법은 Securify입니다. . 오늘은 주로 Oyente와 Securify 두 시스템의 구체적인 아키텍처와 구현 방법에 대해 이야기 할 것입니다. 먼저 Oyente를 살펴 보겠습니다. 왼쪽에서 Oyente의 논리를 볼 수 있습니다. CFG에서 응용 프로그램 후 첫 번째는 탐색기입니다. , 코드의 각 프로세스를 검증하고 정식 검증을 수행합니다. 전체 논리의 흐름을 확인하기 위해 상태가 아니오 또는 예인지 여부. 두 번째 핵심 분석은 실제로 Oyente의 가장 핵심적인 부분입니다.탐색기 경로를 출력으로 변환하고 일부 취약점 검증만 수행합니다.현재는 TOD, Timestamp 종속성 및 Mishandled 예외, 이 세 가지 Verification만 제공합니다.결국 이 시스템은 위양성 및 위음성의 비율을 보장할 수 있습니다.마이크로소프트의 오픈 소스 검증기를 사용하여 전체 아키텍처를 캡슐화합니다.방금 설명한 과정에서 CFG에서 탐색기 검증까지 때때로 우리는 그를 통해 순환해야 합니다. 매번 검증이므로 이 분석 방법은 특히 시간이 많이 걸리고 성공하지 못할 수 있습니다. 이것은 Oyente가 현재 큰 문제를 안고 있는 곳입니다.

이 문제를 기반으로 Securify와 같은 또 다른 방법을 제공합니다.그들은 현재 계약 코드가 실제로 특히 분리하기 쉽다고 믿습니다.기존 코드와 달리 결합도가 특히 높으며 상대적으로 고정된 형태의 계약 코드가 있습니다.우리는 전체 계약 로직을 검사할 필요가 없습니다. 계약 분리의 각 모듈을 분석하여 자동화 정도를 개선합니다. 왼쪽 그림은 전체 검증 프로세스를 보여줍니다. 계약 바이트 코드는 도메인 언어를 통해 전달됩니다. 특히 앞에서 언급한 패턴 매칭과 같은 검증 모듈로 일부 취약점을 검증 언어 패턴 매칭 프레임워크로 변환하고 시맨틱이 이에 호환되는지 검증합니다. 마지막으로 보고서도 주어지는데, 이 자동 감사 방식을 통해 최종적으로 지갑을 출력할 수 있는 관리자를 수정할 수 있습니다.

좀 더 구체적인 포인트는 시맨틱 분석을 어떻게 하느냐 입니다. , 두 번째는 MustFollow, MayFollow는 L2가 L1을 따르는 경로를 가져야 함을 의미하고 MustFollow는 L2의 모든 경로가 L1을 따라야 함을 의미합니다.이 두 가지 차이점은 전체 논리 프레임 워크를 정의합니다.

두 번째는 데이터입니다.계약에서 데이터 변경을 정의하는 방법은 세 가지 유형을 사용합니다.첫 번째 MayDepOn은 두 가지 요소로 하나는 Y라고하고 다른 하나는 T라고합니다.T가 변경되면 Y는 변경되거나 변경되지 않을 수 있습니다. 두 번째는 Eq입니다. 즉, Y는 T에 의해 결정됩니다. 세 번째는 DetBy, Y 및 T는 일대일 대응입니다. T가 Y로 변경되는 한 확실히 변경됩니다. 여기에 더 생생한 상상 방법이 있습니다. 사실 Maydepon은 T 변수와 같습니다. 시간, 일정 기간 동안 Y는 값일 수 있고, T는 변경될 수 있으며, Y는 변경되지 않을 수 있습니다. 세 번째는 일대일 관계입니다. 우리가 해시를 계산하는 것처럼 T를 변경하는 한 Y는 변경되어야 합니다. 논리와 데이터의 2차원을 통해 일부 검증을 수행했으며 최종 검증 모듈은 현재 약 6~7개의 스마트 계약 취약성 검증 언어를 제공합니다.이 언어는 플러그인으로 작성되며 다른 보안 개발자는 계속 검증을 풍부하게 할 수 있습니다. 취약점의 언어. .

결국 자동 감사를 평가할 때 자동화 정도, 오탐율, 오탐률에서 이 문제를 제공해야 합니다. 여전히 수동으로 다시 확인해야 합니다.이 작업은 매우 번거롭고 이 방법을 통해 오탐률을 줄일 수 있습니다.이 두 가지 자동화된 감사 방법은 기호 실행 및 기호 추상화입니다.

마지막으로, 검토를 위해 현재 세 가지 유형의 자동 감사 방법, 기능 코드 일치, 형식 검증, 기호 실행 및 기호 추상화가 있습니다. 전체 분석 과정을 돌이켜보면 현재의 자동화된 감사 방식은 매우 미숙한 단계에 있으며 크게 세 가지 문제에 직면해 있음을 분명히 알 수 있습니다. . . 두 번째는 자동화 정도가 상대적으로 낮아 지속적인 감사가 필요하다는 점, 세 번째는 감사 시간이 상대적으로 길다는 점입니다.

마지막은 우리의 전체 분석을 검토하는 것입니다.먼저 스마트 계약의 개발 상태를 명확히하고 자동 감사 방법을 테스트합시다.좌우에 우리 기술 교류 그룹이 있습니다.관심있는 아이들은 가입을 환영합니다. 함께 더 심도 있는 토론을 합니다. 이것이 제가 오늘 하는 일입니다. 내용을 공유해 주셔서 감사합니다.