최근 ChatGPT가 인기를 끌며 출시 2개월 만에 활성 사용자가 1억 명을 돌파했습니다. 그것을 사용하여 기사를 쓰고, 코드를 작성하고, 사랑에 빠지고, 직업을 찾고, 이메일에 답장하는 것은 일상적인 작업이 되었습니다. 인터넷에서 "돈을 벌기" 위해 이 소프트웨어를 사용하는 방법을 가르치는 많은 방법이 있습니다. 펜실베니아 대학의 Wharton School of Business는 "학생"ChatGPT가 경영 관리 시험에 합격했다고 주장했습니다.

이에 따라 인공지능이 특정 직업을 대체하거나 심지어 인간이 인공지능으로 대체된다는 화두가 화제가 되기도 했고, 모두가 감옥에 갇힌 시대에 모두의 가슴은 점점 뛰고 있다.

그렇다면 인공지능, 즉 공식 검증과 같은 "컴퓨터 제품"이 인간을 대체할 수 있을까요? Web3.0의 세계에서 공식 검증이 수동 검토를 대체할 수 있습니까?

공식 검증

형식 확인은 컴퓨터 프로그램이 예상대로 작동하는지 확인하기 위한 수학적 증명 방법입니다. 프로그램의 속성과 예상되는 동작을 수학 공식으로 표현한 다음 자동화된 도구를 사용하여 이러한 공식이 유지되는지 확인합니다. 이 프로세스는 프로그램이 기대치를 충족하는지 확인하는 데 도움이 됩니다.

공식 검증의 적용

형식 검증은 다음을 포함하여 다양한 시스템에서 널리 사용할 수 있는 도구입니다.

• 컴퓨터 하드웨어 설계: 집적 회로 및 디지털 시스템이 필요한 사양을 충족하고 올바르게 작동하는지 확인합니다.

• 소프트웨어 엔지니어링: 특히 항공, 의료 기기 및 금융 시스템과 같은 미션 크리티컬 애플리케이션/도메인에서 소프트웨어 시스템의 정확성과 신뢰성을 검증합니다.

• 네트워크 보안: 암호화 알고리즘 및 프로토콜의 보안을 평가하고 보안에 민감한 시스템의 보안 격차를 식별합니다.

• AI 및 기계 학습: AI 및 ML 모델의 속성 및 동작을 검증하여 예상대로 수행하고 정확한 예측을 수행하도록 합니다.

• 자동 정리 증명: 수학, 물리학 및 컴퓨터 과학 분야에 적용되는 수학적 정리를 확인하고 수학적 추측을 증명합니다.

• 블록체인 및 스마트 계약: 블록체인 시스템 및 스마트 계약의 정확성, 보안 및 신뢰성을 보장합니다.

스마트 계약의 공식 검증

스마트 계약의 공식 검증은 스마트 계약의 논리와 예상 동작을 수학적 표현으로 표현한 다음 자동화 도구를 사용하여 이러한 수학적 표현이 올바른지 확인하는 것입니다.

이 프로세스에는 다음이 포함됩니다.

• 계약의 사양 및 속성은 공식 언어로 정의됩니다.

• 계약 코드 번역"”를 수학적 논리 또는 모델과 같은 형식적인 표현으로 변환합니다.

• 자동화된 정리 증명기 또는 모델 검사기를 사용하여 계약의 사양 및 속성이 유지되는지 확인합니다.

• 확인 프로세스를 반복하여 오류나 예상과 다른 부분을 찾아 수정합니다.

때때로 자동화된 정리 증명기 또는 모델 검사기는 속성을 증명하거나 반증할 수 없습니다. 이 경우 사양 및 원하는 속성을 구체화하고 검증 프로세스를 반복해야 할 수 있습니다.

사양을 더 작은 코드 조각으로 나누거나 더 많은 사양 정보를 제공하면 사양과 예상 속성을 구체화할 수 있습니다. 이렇게 하면 정리 증명자와 모델 검사자가 사양과 속성이 유지되는지 쉽게 확인할 수 있습니다.

정식 검증은 하나의 계약 또는 동시에 여러 계약에 적용될 수 있습니다. Web3.0 프로젝트는 종종 여러 계약을 사용하며 이러한 계약이 함께 작동하고 원하는 프로젝트 기능을 올바르게 구현하는지 확인하는 것이 중요합니다.

공식 검증에서 이 수학적 방법을 사용하면 속성이 수학적으로 정확한 것으로 엄격하게 입증되었기 때문에 스마트 계약에 버그, 버그 및 기타 예기치 않은 동작이 없는지 확인하는 데 도움이 됩니다.

코드를 공식화하다

코드 스니펫 예제 1

다음 코드는 단순화된 토큰 전송 기능 프로그램을 보여줍니다. 두 명의 사용자가 있으며 각각 약간의 토큰을 가지고 있습니다(balance 및 balance 2). transferFromUser 1 함수는 User 1에서 User 2로 토큰을 전송합니다. 프로그램에는 토큰의 총 공급량이 항상 잔액의 합계와 같다는 불변성이 있습니다.

코드 조각 1: 토큰 전송 프로그램

불변량을 수학 공식으로 표현하고 공식에 번호를 매깁니다. 수학 공식에서 "="는 할당이 아니라 "같음"을 의미합니다.

코드 스니펫 예제 2

다음 코드는 논리 수식을 추가하는 방법을 보여줍니다(예제의 단순성과 명확성을 위해 정수 오버플로는 무시됨).

코드 스니펫 2: 코드의 의미를 표현하는 논리식 함수

transferFromUser 1이 프로그램에서 불변량을 보유하고 있는지 확인하려면 불변량(수식 1)에 대한 수식 7(함수 끝에 있음)을 확인할 수 있습니다. 아래는 고등학교 대수 방법을 사용한 증명입니다.

공식 검증 및 수동 감사의 협업

스마트 계약의 보안을 보장한다는 측면에서 공식 검증과 수동 감사는 서로를 보완한다고 할 수 있습니다.

공식 확인:

공식 검증은 계약의 논리와 동작 및 예상되는 속성을 확인하는 체계적이고 자동화된 방법을 제공하여 잠재적인 버그나 취약점을 쉽게 식별하고 수정할 수 있도록 합니다. 수동 검사로는 감지하기 어려울 수 있는 복잡하거나 미묘한 문제를 찾는 데 매우 효과적입니다.

복잡하거나 여러 계약을 처리할 때 인간이 확인해야 할 모든 조합과 가능성에 대해 추론하기 어려운 반면 기계는 "압력이 없습니다".

수동 감사:

인적 감사는 계약 코드, 설계 및 배포에 대한 전문가 검토를 제공합니다. 감사 전문가는 자신의 경험과 전문 지식을 사용하여 잠재적인 보안 위험을 식별하고 계약의 전반적인 보안 상황을 평가할 수 있습니다.

이 외에도 인간은 공식적인 검증 프로세스가 올바르게 수행되었는지 확인하고 자동화 도구로 감지할 수 없는 문제를 확인할 수 있습니다. 따라서 정식 검증에 사용되는 사양 및 필수 속성의 정확성을 보장하는 데는 전문가의 감사가 더 도움이 됩니다.

요약하면 공식 검증과 수동 감사의 두 가지 방법을 결합해야만 스마트 계약의 보안에 대한 포괄적이고 철저한 평가를 수행할 수 있으며 발견 및 버그 수정 가능성이 높아집니다. 또한 인간과 기계의 장점을 결합한 보안 접근 방식으로 "심층 방어"라고 합니다.

보안 전문가 온라인 AMA

공식 검증의 힘을 과소평가할 수는 없지만 수동 감사의 중요성도 무시할 수 없습니다. ChatGPT 공식 홈페이지에서 자체적인 단점을 인정했고, 인공지능이 인간의 생각과 창조를 대체할 수 없다는 진부한 논의도 여기서 10,000단어를 생략할 수 있다…

마찬가지로 공식 검증은 수동 감사를 대체할 수 없으며 두 가지가 서로를 보완하여 스마트 계약에 대한 완전한 검사를 수행합니다.

기사를 읽은 후 질문이 있습니까? [2월 10일 금요일 일본] [CertiK Twitter AMA]에 게스트로 참석하여 전문가들과 온라인 1:1 질의응답 시간을 가져보세요! 시차로 인해 참석하지 못하는 친구들은 배경에 메시지를 남길 수 있으며, 이를 게스트들에게 전달하여 AMA 다시보기 콘텐츠를 공개합니다!