블록체인이라는 단어는 최근 몇 년 동안 최첨단 기술 개념, 시장의 뜨거운 단어, 과잉 소비의 상징에 이르기까지 여러 가지 기복을 겪었습니다. 많은 사람들은 블록체인이 많은 산업의 페인 포인트를 해결하는 도구이며 차세대 "슈퍼 비즈니스 캐리어"의 탄생을 위한 촉매제가 될 가능성이 있다고 믿습니다.

그러나 전설적인 서사적 변화는 아직 오지 않았고 주목을 받고 있습니다. 관심 있는 사람은 이득을 볼 것이고, 이익을 추구하는 사람은 맹목적으로 돈을 지불할 것입니다. 너무 일찍 여론의 소용돌이에 빠지면 성장 단계에서 기술을 해치고 시험하게 된다.

오늘날 실제 상황은 상륙 응용 프로그램이 거의 없고 기술과 산업 연결 사이에 여전히 거리가 있으며 투기꾼의 소음이 기술과 산업에 진정으로 관심을 갖는 "중추 목소리"를 가렸다는 것입니다. Odaily는 최고의 새로운 비즈니스 미디어 36Kr, 최고의 기술 리더 및 학계 엘리트와 손을 잡고 규제를 수용하는 방법에 대해 논의하고, 산업이 찌꺼기를 제거하고 본질을 추출하도록 홍보하고, 일을 진지하게 하는 사람들에게 트래픽과 목소리를 넘겨주고, 힘을 사용하여 블록체인을 착륙시키십시오.

9월 5일, Odaily가 주최하고 36Kr Group Strategy가 공동 주최한 블록체인 POD 컨퍼런스에서 CertiK의 수석 과학자인 Vilhelm Sjöberg는 "완전히 신뢰할 수 있는 스마트 계약 및 블록체인 생태계 구축을 향하여"라는 제목의 연설을 했습니다.

보조 제목

다음은 CertiK의 수석 과학자인 Vilhelm Sjöberg의 연설 전문입니다.

안녕하세요 여러분, 저는 CertiK의 수석 과학자이며 블록체인에 대한 많은 연구 작업을 수행했습니다. 블록체인은 데이터베이스이며 기술과 신뢰 측면에서 중요한 연구 주제가 많이 있습니다. 프로그램은 실행 오류가 발생하기 쉬운데 왜 실행 오류가 계속 발생합니까? 프로그램을 더 안정적으로 만드는 방법은 무엇입니까? 물론 사람들이 프로그래밍을 잘 못해서가 아니라 스마트 컨트랙트가 블록체인에서 매우 특별하고 중요한 부분이기 때문입니다. 블록체인에서는 스마트 컨트랙트가 한번 배포되면 업데이트가 불가능하며, 배포된 스마트 컨트랙트 자체에 허점이 있다면 해커들이 이 허점을 찾아내어 자산을 훔칠 수 있습니다. 이러한 문제는 우리가 피해야 할 것입니다.

프로그램의 안전을 보장하기 위해 일부는 수동으로 검토되지만 시간 비용이 상대적으로 높고 다른 문제가 발생할 수 있습니다. 물론 감사를 위한 자동 테스트도 있지만 모든 문제를 찾는 데 도움이 되지는 않습니다. 따라서 블록체인의 경우 이러한 솔루션은 여전히 ​​충분하지 않습니다.

CertiK는 수학적 방법을 사용하여 프로그램을 증명합니다. 즉, 정식 검증을 통해 스마트 계약 및 블록체인 응용 프로그램에 대한 보안 서비스를 제공합니다.당사의 동시 운영 체제 커널인 CertiKOS는 완전히 공식적으로 입증될 수 있으며 그 뒤에 있는 핵심 기술은 "심층 사양"입니다.

복잡한 시스템의 경우 CertiK는 심층 사양 기술을 활용하여 안전 인증을 획득합니다.우리는 복잡한 시스템을 계층화하고 각 추상 계층이 작성하는 내용, 수행하는 작업 및 수행하는 작업을 이해하여 올바른 사양을 충족하는지 여부를 증명합니다. 추상화 계층을 작성하면 함께 모아서 확인할 수 있습니다. 추상화 계층을 서로 연결하여 증명을 통합할 수 있습니다. 이것이 우리가 하는 주요 작업입니다. 계층화 및 통합을 통해 완전한 분산형 스마트 계약 검증을 달성하는 것입니다.

당사 운영 프로그램인 CertiKOS의 커널은 여러 계층으로 나누어져 있으며 한번에 하나의 복잡한 기능을 다루기 때문에 크고 복잡한 프로그램의 검증이 가능합니다.

이 사진은 우리가 Landshark 머신에 운영 체제 CertiKOS를 배포했음을 보여줍니다.

우리는 또한 학계의 많은 전문가들과 협력해 왔으며 그러한 프로젝트를 개발하는 데 도움을 줍니다. 2015년 Gu Ronghui 교수와 Shao Zhong 교수는 "깊은 사양"의 개념을 제안하고 이를 검증했습니다. 2016년에 우리는 이미 바로 사용할 수 있는 이 제품과 서비스를 기업에 판매하고 있었습니다. 2017년에는 스마트 계약을 검증하기 위해 CertiK를 확장했습니다. 따라서 학술 연구도 수행할 수 있고 블록체인에 대한 공식적인 검증도 수행할 수 있습니다.

다음으로 스마트 계약 검증을 위한 프로그래밍 언어인 DeepSEA라는 현재 진행 중인 연구 프로젝트에 대해 자세히 소개하겠습니다.

그 전에 이해를 돕기 위해 정식 검증이 무엇인지 이야기 해 봅시다.형식 검증에는 얕은 검증과 심층 검증을 포함하여 다양한 검증 기술이 포함됩니다.

얕은 수준의 검증은 스마트 계약의 매우 일반적인 정수 오버플로 문제와 같은 몇 가지 일반적인 검증을 말합니다.상대적으로 얕은 검증을 위해 스마트 계약을 자동으로 스캔하고 취약성을 찾는 데 도움이 되는 1세대 고성능 스마트 계약 자동 탐지 엔진 CertiK AutoScanEngine(CASE)을 설계했습니다. 분산 검증은 계약을 다른 모듈로 세분화하여 완료됩니다. 사용자는 우리의 검증 엔진에 컨트랙트를 업로드하여 특정 메서드를 호출할 때 어느 것이 올바른지 또는 오류가 발생했을 때 어떻게 처리하는지 확인할 수 있습니다. 전체 프로세스는 인력에 거의 의존하지 않고 최대 기계 검증을 달성합니다.

다음으로 심층 검증에 대해 이야기하고 싶습니다.예를 들어 가치의 속성을 확인해야 하고 이를 증명하는 방법에 대해 생각해야 합니다. 특정 아키텍처 또는 특정 메서드에 적용될 수 있는 일부 로컬 속성이 있습니다. 그러나 심층 검증을 통해 모든 스마트 계약의 전체 생태계에 적용될 수 있습니다. 백서에 설명된 대로 전체 블록체인 생태계에 보안을 제공하는 것을 목표로 일부 결제 시스템, 온체인, 오프체인 등 다양한 체인을 통합하고 결합할 수 있습니다.

때때로 우리는 전적으로 기계에 의존할 뿐만 아니라 일부 사람의 개입에 의존하기도 합니다.예를 들어 복잡한 시스템의 경우 설명서에 사양을 작성해야 합니다.CertiK에서 각 시스템은 서로 다른 계층으로 나눌 수 있습니다. 따라서 그러한 프로젝트는 심층 검증 및 사양 시스템을 만드는 데 도움이 될 수 있습니다. 이를 위해 자체 언어 DeepSEA를 개발했습니다. 계약서만 작성하고 싶다면 개인화된 언어로 작성할 수 있습니다. 그러나 신뢰도가 높은 일부 계약의 경우 다른 측면에서 신뢰도가 높지 않을 수 있습니다. 물론 EVM의 언어로 작성할 수 있지만 그다지 신뢰할 수 있는 코드는 아닙니다. 그래서 우리는 원래 CertiK를 작성하기 위해 개발된 CertiK의 언어 DeepSEA를 출시했으며 이제 이더리움 계약에도 매핑할 수 있습니다. 사양을 생성할 수 있을 뿐만 아니라 검증된 컴파일러를 사용할 수도 있습니다.

블록체인에는 우리가 하는 모든 일이 올바른지 확인하는 계약이 있습니다. 따라서 우리가 심도 있는 수준에서 유효성 검사를 수행하고 있는 일부 절차에 대한 매우 좋은 시연이라고 생각합니다. 자세히 알아보려면 계약이 올바르고 양호한 상태인지 확인하는 데 도움이 되는 몇 가지 단계를 수행해야 합니다. 그래서 우리는 이 개념을 적고 최종적으로 이러한 일련의 단계를 통해 계약의 정확성을 보장할 수 있습니다.

온라인에서도 볼 수 있는 다른 프로젝트가 있습니다. 우리가 확장할 수 있는 몇 가지 지불 관련 프로젝트가 있습니다. 스마트 계약, 컴파일러 및 EVM 모델과 관련된 프로젝트도 있습니다. 아래에 나열된 다음 영역에서 우리는 당신을 도울 것입니다. 관심이 있는 경우 파트너로 가입하고 계속 연락할 수 있습니다. 다들 감사 해요!