solidity static analysis

잔류/몫 분석을 통한 정적 분석

https://github.com/shaunazzopardi/solidity-cfg-builder 및 https://github.com/gordonpace/contractlarva를 기반으로하는 견고성 스마트 계약 검증을위한 정적 분석.

개요

이 도구는 견고성 스마트 계약의 속성을 완전히 입증하려고 시도하며, 부분적으로 성공시 Soldity Smart 계약으로 입증 된 잔여 속성을 반환합니다.

우리는 견고성 스마트 계약의 제어 흐름 (견고성 -CFG 빌더 및 가변 상태를 기반으로 한 스마트 계약의 속성을 정적으로 증명하기 위해 Solidity Smart 계약의 제어 흐름 그래프 표현을 사용합니다.

이는 Prepost 2017의 EPCTS 시리즈에서 제시된 작업을 부분적으로 기반으로하며 ARXIV에서 사용할 수 있습니다.

분석에 대한 자세한 설명

1. 각 스마트 계약 함수는 트리플을 포함하는 트리플을 태그로 전환 된 컨트롤 흐름 오토 마톤 (CFA)으로 표시됩니다. (i) 프로그램 변수 상태의 조건; (ii) 프로그램 변수 상태를 변환하는 진술; (iii) 성명서의 실행시 활성화 된 재산 이벤트.

2. 각각의 오토 마턴은 프로그램의 초기, 호출 또는 종료 상태에서 모든 이벤트가 발생할 수있는 추상 전환 (속성 이벤트에 의해서만 태그)으로 보강됩니다. 이는 프로모션 내 분석의 기초로 사용됩니다. 각각 이러한 오토 마톤은 해당 함수를 호출하는 스마트 계약의 모든 실행을 과도하게 대략적으로 배치합니다. 이 오토 마톤을 ACFA ( Abstract Control-Flow Automaton )라고합니다.

3. 간단한 주장 전파 알고리즘은 주장에 영향을 줄 수있는 진술이 발생할 때까지 CFA의 명시 적 상태를 통해 프로그램 변수 상태 (조건 및 진술에 의해 암시)에 대한 어설 션을 전파합니다. 이것은 소리입니다.

4. 속성은 트리플의 태그로 전환을 사용하는 동적 이벤트 오토 마톤 (DEA)으로 표시됩니다. (i) 이벤트; (ii) 재산 변수 상태에 대한 경비대; 및 (iii) 속성 변수 상태에 대한 조치.

5. 가변 추상화를 갖는 ACFA는 DEA로 구성되며, CFA 및 DEA 전환 쌍으로 태그가 지정된 전이 또는 # 기호를 포함하는 위치 중 하나를 갖는 추상 모니터링 시스템 (AMS)을 생성합니다. CFA 전이 대신 #을 사용하면 추상 전환의 일치를 나타내며 DEA 전환 대신 DEA 전환 일치가 신호를 보내지 않습니다.

6. 그런 다음 주어진 DEA에 대한 프로그램의 각 기능에 대해 AMS가 생성됩니다.

7. SMT 솔버 인 Z3은 AMS를 구성하는 동안 비행기에서 호출되어 주어진 전환이 실제 실행에서 해당 지점에서 활성화 될 수 있는지 여부를 결정합니다. CFA-DEA 전환 쌍이 주어지면 DEA 가드가 CFA 전환 조건으로 업데이트 된 소스 상태의 변수 추상화에 대해 진실 할 수 있는지 확인합니다. CFA-# 쌍이 주어진 반면, 우리는 CFA 전이 조건으로 업데이트 된 소스 상태의 가변 추상화 가이 시점에서 활성화 된 DEA 전이의 경비병 분리의 부정과 일치하지 않는지 확인합니다 (동일한 DEA 상태로부터 발신 한 DEA 전이는 상호 배타적으로 보장된다).

8. 각 AMS는 CFA-DEA 전이 쌍을 식별하기 위해 분석되어 이러한 방식으로 사용 된 DEA 전이를 추출하여 # 자리 표시 자와의 DEA 전환 일치를 무시합니다. 이러한 DEA 전이의 결합은 원래 DEA의 잔류를 생성합니다. 이것은 때때로 잔류 DEA의 신디케이트 분석을 통해 더욱 감소 될 수 있습니다.

9. 또한, AMSS에서 우리는 DEA Transition의 가드를 제거 할 수있는시기 (즉, TRUE 로 변경)를 식별 할 수 있습니다. 즉, AMS에서 사용할 수있을 때마다 항상 사용됩니다.

10. 생산 된 잔차에 전환이 없으면 속성이 입증되었습니다.

제한

1. 우리는 기능 수정 자 및 스마트 계약 상속을 다루지 않습니다 (분석 가능).
2. DEA 스크립트가 완전히 지원되지 않음 :
   • DEA 변수 상태는 무시됩니다 (분석에서 고려 된 프로그램 상태의 조건 만);
   • 스크립트의 "dea {...}"부분 만 지원됩니다.
3. 통화 상태에 도달하면 프로그램 상태에 대한 모든 알려진 주장이 제거됩니다.
4. v0.4.* 견고성 코드.

요구 사항

1. (필수) Z3 경로에서 실행 파일 (스마트 계약에 대한 주장을 증명하기 위해);
2. (선택 사항) GraphViz (CFA, ACFA 및 AMSS를 시각화하기 위해) 또는 http://webgraphviz.com/을 사용하십시오.

도구 구축

요구 사항 : Cabal v2.4.* (예 : 전체 Haskell 플랫폼 설치)

편집 : 여기에서 지침을 따르십시오

도구 사용 :

올바른 결과를 얻으려면 항상 Solidity Code가 Solidity 컴파일러와 컴파일되는지 확인하십시오.

도구를 사용하려면 Smart Contract Solidity 파일, DEA 속성 파일 및 출력의 선호하는 위치를 실행 파일로 전달합니다.

./main "./examples/courierservice.sol" "./examples/courierservicespec.dea" "cfa.txt" "acfa.txt" "ams.txt" "grestual.dea"

특허

이 프로젝트는 Apache 2.0 라이센스의 조건에 따라 라이센스가 부여됩니다.