개시하다

며칠 전에 열린 The IEEE Blockchain-2020에서 이더럼 Smart Contract의 취약성 Re-entrancy의 해석 기법에 관한 논문이 채택되었기 때문에 개요를 대략적으로 쓰고 싶습니다.
이것은RA(Re-entrancy Analyzer) 도구로 공개입니다.
또 arXiv 논문도 공개됐다.

초개요

분석 방법을 3행으로 정리하면...
1. 아날로그 인코딩
2. 함수 호출의 실행 경로와 Re-entrancy 공격을 통해 호출된 함수 호출의 실행 경로만 추출
3. 양자 비교
네.
둘 다 차이가 없으면 리엔타란시가 없고, 차이가 있으면 리엔타란시가 있다.

이른바 Re-entrancy

Etherm Smart Contract의 대표적인 취약성으로, 불법 함수의 반복 호출을 초래합니다.이더뮤 사상 최대 사건인'더 DAO'에서 이 허점을 부각한 탓에 프레임의 송금 처리를 반복해 큰 피해를 줬다.
Ethereum Smart Contract Best Practices에 실린 코드의 예는 다음과 같다.이것은 은행 작용의 구조적 화폐 추출 처리 함수를 가정했다.

// INSECURE
mapping (address => uint) private userBalances;

function withdrawBalance() public {
    uint amountToWithdraw = userBalances[msg.sender];
    (bool success, ) = msg.sender.call.value(amountToWithdraw)(""); // At this point, the caller's code is executed, and can call withdrawBalance again
    require(success);
    userBalances[msg.sender] = 0;
}

공격의 포인트를 정리하면 이런 느낌이다.

사용자의 잔액이 복원(마지막 줄) 전에 송금 처리를 한다(밑의 세 번째 줄).

이더세움에서 구조기에서 다른 구조기로 보내는 송금과 함수 호출은 모두 구조기 호출로 같다.

함수 호출 기간에 지정한 함수가 없으면fallback 함수라는 무함수를 실행합니다.

일반 송금 처리에서 호출된 함수를 지정하지 않기 때문에fallback 함수를 실행합니다.

공격자는 자신이 준비한 구조의 fallback 함수에서 피해자 구조기의 함수 withdraw Balance를 호출한다.

종합적으로 말하면 사용자 잔액이 리셋되기 전에 송금 처리는 점차적으로 집행되고 피해자 구조기가 가지고 있는 암호 화폐는 흡수된다.

실행 기호(코드 시뮬레이션)

코드 시뮬레이션은 기호 실행 방법(symbolic exection)을 사용합니다.
매개변수와 같은 코드에서 불확실한 값을 기호 변수의 임의 값으로 표시하는 변수를 사용하여 위연산을 수행합니다.실행 기호를 통해 프로그램이 취할 수 있는 모든 상태를 전면적으로 검색할 수 있다.
RA에서는 Solidity가 아닌 EVM(Etherm Virtual Machine) 명령이 기호 변수를 처리할 수 있는 형태로 구현돼 구축된 기호 실행이 이뤄졌다.

경로 조건식(실행 경로)

경로 조건식(path condition)은 프로그램이 어떤 상태에 도달하기 전에 반드시 만족해야 하는 조건식이다.
예를 들어 다음python 코드가 있다고 가정하십시오.

if 0 <= a:
    return 1
else:
    return 0

이 코드 경로의 그림은 다음과 같습니다.

프로그램의 시작은 반드시 실행될 것이기 때문에 최초의 경로 조건식은 항진이다.
return0에 도착하는 줄은 a<0이 필요하기 때문에 이 블록의 경로 조건식입니다.또한return1의 블록에 도달하려면 0<=a가 필요합니다. 이것은 블록의 경로 조건 공식입니다.
이렇게 하면 조건의 불일치가 증가함에 따라 경로 조건식은 복잡해진다.

경로 조건 비교

Re-entrancy를 검색하려면 일반적으로 실행되는 경로 조건식과 Re-entrancy 공격이 발생할 때의 경로 조건식을 비교하십시오.두 사람의 인상은 다음과 같다.

왼쪽은 보통, 오른쪽은 Re-entrancy 공격.오른쪽 공격 프레임은 간단한 함수 호출만 합니다.따라서 Re-entrancy가 없는 함수에 대해서는 왼쪽과 오른쪽 결과가 일치합니다.Re-entrancy가 있으면 함수 호출이 성공했을 때 만족해야 하는 조건은 일반적인 함수 호출과 다르고 최종 경로 조건식은 좌우로 다르다.엄밀히 말하면 프로그램의 단말기 상태는 당연히 여러 개가 있다. 각자 경로 조건식이 있기 때문에 왼쪽과 오른쪽 경로 조건식이 항등식이 될 수 있는지에 따라 일치 판정을 한다.

여담

이것은 사실 내 학창시절의 연구야, 헤헤

여담2

나는 오랜만에 코드를 github에 다시 전송하고 완전히 낯선 사람의 계정으로 제출했다.그런 일이 있었어?징그럽다.과거의 약속을 취소해도 사라지지 않는다.도와주세요.