|DỰ ÁN| TỔNG QUAN CERTORA

CERTORA

CERTORA LÀ GÌ?

Certora là dự án cung cấp công nghệ xác minh chính xác hoàn toàn tự động (auto audit code) và tiết kiệm chi phí cho các hợp đồng thông minh trên các blockchain.

SẢN PHẨM CỦA CERTORA

CERTORA

Xác minh hợp đồng thông minh liên tục (CFV) 

Dành cho các doanh nghiệp sử dụng Hợp đồng thông minh: CFV liên tục giám sát tất cả các hợp đồng để tìm các lỗ hổng mới được phát hiện hoặc các thay đổi có thể làm lộ ra các vấn đề mới.

CFV đảm bảo lâu dài cho tài sản kỹ thuật số trong chuỗi khối bằng cách thông báo ngay lập tức về bất kỳ vấn đề nào, do đó giảm thời gian phản hồi sự cố. Điều này cho phép doanh nghiệp tránh được hậu quả của các giao dịch không mong muốn không thể đảo ngược, hoặc các cuộc tấn công của hacker.

Môi trường phát triển chất lượng (QDE)

Dành cho nhà phát triển: cho phép nhà phát triển phát hiện các vấn đề trong quá trình phát triển, tối đa hóa bảo mật vào thời điểm triển khai hợp đồng.

QDE tự động tạo báo cáo về các vấn đề hiện có, báo cáo mức độ nghiêm trọng của chúng và cách thức chính xác mà chúng tái tạo.

CÔNG NGHỆ NỔI BẬT

Certora có công nghệ độc đáo là Certora Prover có khả năng kiểm tra tại thời điểm biên dịch rằng tất cả các lần thực thi Hợp đồng thông minh có đáp ứng một bộ quy tắc bảo mật hay không.

Công nghệ Certora Prover (AEV- tự động xác minh chính xác) có sẵn như một công cụ bổ sung cho các trình biên dịch và trình gỡ rối hiện có của Hợp đồng thông minh. Nó kiểm tra xem các hợp đồng có tuân thủ các yêu cầu về giao diện của các hợp đồng khác hay không. Công nghệ Prover độc lập với ngôn ngữ và không có ngôn ngữ của Certora xác định chính xác các lỗi trong Hợp đồng thông minh và chứng minh sự vắng mặt của chúng.

Certora Prover cung cấp phạm vi bảo hiểm đường dẫn hoàn chỉnh cho một tập hợp các quy tắc an toàn do người dùng cung cấp.

Ví dụ: một quy tắc có thể kiểm tra xem chỉ một số lượng lớn token có thể được đúc(mint) trong hợp đồng ERC20. Nó(prover) đảm bảo rằng một quy tắc được giữ trên tất cả các đường dẫn và tất cả các đầu vào hoặc tạo ra một đầu vào thử nghiệm chứng tỏ sự vi phạm quy tắc.

CERTORA

Với các đặc trưng:

  • Cảnh báo sai tối thiểu: Các lỗi được báo cáo là có thật
  • Đảm bảo tính đúng đắn về mặt chính thức: Đối với các quy tắc đã được chứng minh, không có cảnh báo bị bỏ lỡ
  • Hoàn toàn tự động: Không cần sự can thiệp của cong người
  • Nhanh chóng: Hỗ trợ các chương trình tùy chỉnh và tích hợp CI/Cd

ĐỘI NGŨ PHÁT TRIỂN

  • Mooly Sagiv – Đồng sáng lập – CEO: Giáo sư và là Chủ nhiệm Hệ thống Phần mềm tại Trường Khoa học Máy tính tại Đại học Tel-Aviv với 30 năm kinh nghiệm về các phương pháp chính thức và phân tích mã tĩnh. Anh ấy đã đóng góp các kỹ thuật được tích hợp vào công cụ xác minh trình điều khiển thiết bị của Microsoft và công cụ Panaya ERP được Infosys mua lại. Anh ấy cũng là đồng thiết kế của Ivy . Anh ấy là thành viên của ACM và là người nhận Giải thưởng Xuất sắc của Microsoft cho những đóng góp cho các phương pháp chính thức. Sagiv là người nhận tài trợ uy tín nhất Châu Âu . Ông có hơn 200 ấn phẩm học thuật với Google H-index 55.
  • Shelly Grossman – đồng sáng lập – Giám đốc công nghệ: Người đam mê chuỗi khối có kiến ​​thức nền tảng về Xác minh chính thức. Cô cũng là một kỹ sư phần mềm giàu kinh nghiệm đã có 5 năm làm việc tại Check Point . Shelly là tác giả chính của kỹ thuật phân lập để đảm bảo tính đúng đắn của lập luận mô-đun. Cô tốt nghiệp chương trình xuất sắc bậc đại học Adi Lautman và là ứng viên Tiến sĩ về Xác minh Hợp đồng Thông minh tại Đại học Tel Aviv.
  • John Toman: nhận bằng Tiến sĩ năm 2019 tại Đại học Washington. Nghiên cứu của Tiến sĩ Toman tập trung vào việc đưa sức mạnh của xác minh tự động vào thế giới thực, các môi trường công nghiệp. Nghiên cứu tập trung vào tác động từng đoạt giải thưởng của ông đã được xuất bản trong một số hội nghị hàng đầu trong lĩnh vực này.
  • Yoav  Rodeh:nhận bằng Tiến sĩ về xác minh chính thức từ Viện Weizmann dưới sự giám sát của Amir Pnueli, người đoạt giải Turing. Trước đây làm việc tại Google và trong nhóm xác minh chính thức của IBM.
  • Nathan Tribble:  tốt nghiệp MSU Denver với bằng Cử nhân Kỹ thuật Điện tập trung vào Phần mềm Nhúng và Kỹ thuật Mạng và Khoa học Máy tính tập trung vào Phát triển Ứng dụng Web với trẻ vị thành niên về Toán và Lý thuyết Âm nhạc. Nathan đã dành 16 năm trong lĩnh vực CNTT trong các lĩnh vực từ phát triển web Full-Stack đến Giải pháp Phần cứng / Phần mềm tùy chỉnh cho Viễn thông hạm đội và Kiến trúc Giải pháp Doanh nghiệp.
  • Michael  George: Tiến sĩ Đại học Cornell, từng là giảng viên trong 7 năm. Ông đã giảng dạy các khóa học về mọi thứ, từ toán học rời rạc đến lập trình chức năng và hệ điều hành. Ông có nhiều mối quan tâm trong khoa học máy tính, bao gồm xác minh chính thức, thiết kế ngôn ngữ lập trình và hệ thống phân tán.
  • Eldad Peretz: là Thạc sĩ Khoa học Máy tính sinh viên Đại học Tel Aviv. Anh ấy có nhiều sở thích về Khoa học Máy tính và gần đây đã tập trung vào lý thuyết độ phức tạp và học máy. Eldad làm việc với chúng tôi như một phần của kỳ thực tập mùa hè cho đến khi anh ấy gia nhập IDF.
  • Nick  Armstrong: có bằng Kỹ sư Máy tính tại Đại học Washington, nơi anh tập trung vào sự kết hợp giữa bảo mật và người máy với nghiên cứu về Tương tác với người máy. Sau khi tốt nghiệp, anh dành thời gian phát triển phần mềm bảo mật và mã hóa máy tính trước khi gia nhập Certora.
  • Aleksander Kryukov:đã nghiên cứu Tính tin cậy của Hệ thống Nâng cao khi còn là một sinh viên EMJMD. Anh tốt nghiệp với bằng MS vào tháng 9 năm 2021 tại Đại học University of Lorraine (lý luận chính thức) và Đại học St Andrews (kỹ thuật phần mềm). Có bằng Cử nhân Công nghệ Thông tin và Kỹ thuật Máy tính tại Đại học Southwest State (Kursk, Nga).
  • Ariel Grosh: đang làm việc với tư cách là một nhà nghiên cứu bảo mật. Đồng thời, anh ấy đang theo học chương trình cử nhân của mình về Khoa học Máy tính và Toán học tại Đại học Bar Ilan.
  • Uri Kirstein: là một Kỹ sư Phần mềm tốt nghiệp kiêm cử nhân Kỹ thuật Máy tính tại Technion. Anh ấy đã làm việc hai năm tại Apple trong nhóm CAD.
  • Sitvanit Ruah: nhận bằng Tiến sĩ trong quá trình xác minh chính thức từ Viện Khoa học Weizmann dưới sự giám sát của Amir Pnueli, người đoạt giải Turing. Cô là tác giả của 15 bài báo và 11 bằng sáng chế. Trước đây cô đã làm việc trong nhóm xác minh chính thức của IBM Research và KayHut. Sitvanit có nhiều kinh nghiệm trong việc xác minh chính thức và phân tích tĩnh.
  • Chandrakana Nandi: Tốt nghiệp Tiến sĩ về Ngôn ngữ Lập trình và Kỹ thuật Phần mềm tại Đại học Washington. Trong thời gian tiến sĩ, cô tập trung vào việc phát triển DSL, trình biên dịch và trình tổng hợp chương trình cho hình học tính toán. Tác phẩm của cô ấy đã giành được một số giải thưởng bao gồm Học bổng của Adobe và Giải thưởng Giấy hay nhất POPL.

CERTORA

ĐỐI TÁC

Đối tác là các quỹ lớn:  A.Capital VenturesSemantic VenturesVMwareCoinbase VenturesElectric Capital, .

Các khách hàng của CertoraCoinbaseCompound Finance, CeloOrchidAAVEOpyn, TBTC, BalancerSynthentix, Origin, Dforce, Sushiswap, Furucombo, Syndicate, Maker, Notional, Rolla, Paraswap, Indexed Finance, BenQiOrca, OpenZeppelin. ..

ĐỐI THỦ CẠNH TRANH

Không giống như các công cụ thực thi tượng trưng chọn các đường dẫn cụ thể và một tập hợp các mẫu xấu cố định: MythX và Slither, Certora Prover cung cấp phạm vi bảo hiểm hoàn chỉnh cho bộ quy tắc do người dùng cung cấp.