Uniswap V3 거래 프로토콜: MetaTrust Labs가 최초의 형식 검증을 성공적으로 구현했습니다

저자: MetaTrust Labs

MetaTrust Labs는 최근 Xcalibyte의 요청에 따라 Uniswap V3 Swap 프로토콜의 주요 부분에 대한 형식 검증을 완료했습니다. 이 검증은 Uniswap의 소스 코드를 엄격하게 분석하고, 수학적으로 Uniswap V3 백서에 설명된 예상 금융 모델이 올바르게 구현되었음을 증명합니다.

Uniswap의 복잡한 코드와 모델을 검증하기 위해 MetaTrust Labs는 자체 개발한 혁신적인 분석 도구를 활용했습니다. 다음은 팀이 검증을 수행한 과정입니다.

Web 3.0 보안 연구의 일환으로, 우리는 Uniswap V3의 대부분에 대해 형식 검증을 수행했습니다.

우리는 먼저 우리의 검증 도구가 지원하는 명세 언어를 사용하여 Uniswap V3 소스 코드의 형식 모델을 구축했습니다. 둘째, 우리는 Uniswap 형식 모델이 충족해야 하는 속성을 정의하기 위해 우리의 도구에서 정의한 논리를 사용했습니다. 이러한 속성은 Uniswap V3 백서에 설명된 금융 모델을 형식화하며, 여기에는 이산 적분과 같은 복잡한 수학 개념이 포함됩니다.

Uniswap V3의 금융 모델의 복잡성 때문에, 표준 검증 도구는 Uniswap 코드가 수학 모델을 올바르게 표현하고 있음을 증명할 수 없습니다. 우리의 도구는 이렇게 복잡한 시스템을 설명하고 검증하기 위해 최첨단 검증 기술을 사용합니다.

기술적으로, 이 도구는 데이터 정제를 결합한 고차 분리 논리를 사용하여 자동 검증을 구현하며, Isabelle/HOL 정리 증명기에서 형식적으로 정의되고 구현됩니다.

기존 방법과 비교할 때, 첫째, 정리 증명기에 기반한 형식 검증은 형식 정의의 의미와 추론 시스템 덕분에 가장 신뢰할 수 있는 신뢰 기반을 가지고 있습니다. 둘째, 유효한 표현력을 가진 고차 분리 논리 위에 구축된 추론 시스템은 Uniswap V3 백서에 설명된 이산 적분과 같은 금융 모델의 고수준 규약을 표현하고 검증할 수 있게 해줍니다. 이는 전통적인 검증 도구인 Solidity에 내장된 SMT 검증기가 도달할 수 없는 영역입니다.

이번 성공은 복잡한 DeFi 시스템의 감사에서 맞춤형 검증 도구의 가치를 강조합니다. 수학적으로 기반이 있는 검증은 차세대 신뢰할 수 있고 널리 사용되는 DApp을 가능하게 합니다.

MetaTrust Labs의 David는 "우리는 이 중요한 성과에서 핵심적인 역할을 한 분석 능력을 제공하게 되어 자랑스럽습니다. 이러한 수준의 형식 검증은 블록체인 소프트웨어의 투명성과 신뢰성에 대한 새로운 기준을 설정합니다."라고 말했습니다.

MetaTrust Labs의 Uniswap V3 Swap 프로토콜에 대한 형식 검증은 DeFi 생태계에 있어 획기적인 발전이며, Uniswap 사용자에게는 플랫폼을 신뢰하고 사용할 더 많은 이유를 제공합니다.

검증에 대한 자세한 정보는 여기서 확인할 수 있습니다.

MetaTrust Labs

지금 무료 사용하여 MetaScan으로 계약의 안전을 보호하세요.