EthSystems가 이더리움(ETH) 프라이버시 풀의 설계 문서부터 세폴리아 테스트넷에서 실행되는 코드까지 형식 검증을 마쳤다. 검증 과정에서 문제 6건을 발견했으며, 이 가운데 3건은 검증 도구 자체에서 나왔다.
EthSystems는 27일 이 같은 결과를 발표했다고 PANews는 전했다. 프라이버시 풀은 거래 정보를 가리면서도 거래가 정해진 규칙을 따르는지 확인하도록 설계된 기술이다. 이번 검증은 설계 문서의 내용이 실제 구현과 배포 코드에 이어지는지 단계별로 점검했다.
형식 검증은 프로그램이 충족해야 할 조건을 수학적으로 표현하고, 그 조건이 성립하는지 도구로 확인하는 방법이다. EthSystems는 모델·회로·해시 검증에 Lean을, 스마트계약 검증에 Halmos와 Kontrol을 사용했다. 지갑은 Aeneas와 Verus로 살폈다.
검증기와 배포 단계에서는 코드를 다시 만들어 세폴리아 테스트넷에서 실행되는 바이트코드와 바이트 단위로 대조했다. 바이트코드는 네트워크가 실제로 실행하는 코드다. 이 절차로 설계 문서와 사람이 읽는 코드의 검토 결과가 배포된 코드에도 반영됐는지를 확인했다.
핵심 검증 대상은 이중 지출 방지와 가치 보존이다. 같은 자산을 두 번 쓰거나 거래 과정에서 근거 없이 가치가 늘어나는 일을 막는 조건이다. EthSystems는 두 조건을 Lean 정리 증명기로 기계 검증했다고 밝혔다.
검증 과정에서 문제 6건이 발견됐고, 이 가운데 3건은 검증 도구에서 나왔다. EthSystems는 발표에서 개별 문제의 내용이나 수정 여부는 공개하지 않았다.
검증 결과에는 전제가 남아 있다. PANews는 EthSystems가 검증 결과의 전제로 해시 충돌 부재, 위조 증명 거부, 스마트계약과 검증 모델의 동작 일치를 들었다고 보도했다. 따라서 검증 결과는 이 조건들이 유지되는 범위에서 해석해야 한다.
이더리움 공용 장부에서 거래 정보가 공개되는 문제를 다루기 위해 EthSystems는 기관용 프라이버시 기술을 개발하고 있다. 이번 발표는 설계 문서부터 테스트넷 실행 코드까지 검증한 범위와 함께 남은 가정을 공개했다.
<Copyright ⓒ TokenPost, unauthorized reproduction and redistribution prohibited>
Most Popular