Certora là gì? Tổng quan về dự án Certora

Tổng quan

Certora sinh ra để giải quyết những vấn đề của Hợp đồng thông minh (Smart contract); một trong số đó là xác thực và bảo mật. Được Coinbase Ventures đầu tư trong vòng gọi vốn Series A. Với công nghệ xác minh chính xác hoàn toàn tự động cho các hợp đồng thông minh.

Vậy Certora là gì? Hãy cùng GFS Blockchain tìm hiểu qua bài nghiên cứu dưới đây nhé!

Certora

Certora là gì?

Certora cung cấp các công cụ phân tích bảo mật và xác minh chính thức có thể truy cập; tiết kiệm chi phí của các hợp đồng thông minh.

Đội ngũ phát triển

Certora được xây dựng dựa trên 30 năm nghiên cứu học thuật và hàng trăm ấn phẩm học thuật đi tiên phong trong lĩnh vực Xác minh. Nhóm nghiên cứu kết hợp khả năng lãnh đạo học thuật, sức mạnh công nghiệp và chuyên môn về Blockchain.

Certora

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.

Cố vấn

Alex Aiken: Giáo sư Khoa học Máy tính của Alcatel-Lucent tại Stanford. Alex nhận bằng Cử nhân Khoa học Máy tính và Âm nhạc tại Đại học Bowling Green State năm 1983 và bằng Tiến sĩ. từ Đại học Cornell vào năm 1988. Alex là Nhân viên Nghiên cứu tại Trung tâm Nghiên cứu Almaden của IBM (1988-1993) và là Giáo sư trong khoa EECS tại UC Berkeley (1993-2003) trước khi gia nhập giảng viên Stanford vào năm 2003. Mối quan tâm nghiên cứu của anh ấy là trong các lĩnh vực liên quan đến ngôn ngữ lập trình. Anh ấy là Thành viên ACM, người đã nhận được Giải thưởng Giảng dạy của Phi Beta Kappa, và từng là chủ tịch Khoa Khoa học Máy tính Stanford (2014-18).

GIÁO SƯ Jeff Flowers: Ông là Giám đốc Chương trình giảng dạy và Hướng dẫn tại Đại học Blockchain và tiếp tục giảng dạy tại DLT Education về lĩnh vực mới nổi của Blockchains. Tại Certora, Jeff cung cấp một ống kính được tạo ra từ nhiều dự án dựa trên Blockchain và DLT mà anh ấy liên kết, cũng như là thành viên tích cực của nhiều cộng đồng tập trung vào công nghệ xung quanh Thung lũng Silicon.

Avita Gatt: hơn 25 năm kinh nghiệm trong ngành trong lĩnh vực Con người lãnh đạo các công ty tăng trưởng cao trên toàn cầu – hỗ trợ và phát triển môi trường khởi nghiệp giai đoạn đầu. Cô đã thành lập và nhân viên các công ty con toàn cầu, giúp xây dựng đội ngũ điều hành toàn cầu và phát triển văn hóa công ty sáng tạo, chuyên nghiệp cao và gắn bó với nhau. Bà đã dẫn đầu 6 thương vụ hợp nhất M&A nhân sự thành công. Aviva có bằng Cử nhân Công tác xã hội của trường Đại học Hebrew U và bằng Thạc sỹ Quản trị Kinh doanh về Quản lý & Nhân sự của Đại học Bách khoa NY.

Tiến sĩ Yona Hollander: chuyên gia và doanh nhân dày dạn kinh nghiệm trong ngành, ông có hơn 20 năm kinh nghiệm quản lý và công nghệ trong không gian an ninh mạng. Yona là người đồng sáng lập Fortsacle trong lĩnh vực Phân tích hành vi người dùng (UBA) được RSA mua lại vào năm 2018. Trước khi thành lập Fortscale, anh đã thành lập và quản lý Cyber Security, một công ty tư vấn công nghệ cửa hàng. Yona cũng là người sáng lập và từng là Phó chủ tịch Nghiên cứu Bảo mật tại Entercept, được McAfee mua lại vào năm 2003 với giá 120 triệu đô la. Sau đó, Yona tiếp tục làm Phó Giám đốc Nghiên cứu Bảo mật tại McAfee HQ ở Santa Clara. Từng là Phó Giám đốc Phát triển Kinh doanh tại Netect, công ty tiên phong trong công nghệ đánh giá lỗ hổng bảo mật, được mua lại bởi BindView vào năm 1999. Yona có bằng Tiến sĩ. trong Khoa học Máy tính của Viện Công nghệ Israel (Technicon).

GS Neil Immerman: Nhà khoa học máy tính nổi tiếng nghiên cứu logic trong khoa học máy tính và độ phức tạp trong mô tả. Ông nhận bằng BS và MS từ Đại học Yale vào năm 1974 và bằng Tiến sĩ của mình. từ Đại học Cornell vào năm 1980. Cuốn sách Mô tả Phức tạp của ông xuất hiện năm 1999. Ông đã nhận được Giải thưởng Göedel cho việc giải một bài toán mở trong 20 năm trong lý thuyết khoa học máy tính. Immerman là Thành viên ACM và Thành viên Guggenheim .

Daniel Jackson: Giáo sư Khoa học Máy tính tại MIT, đồng giảng dạy MacVicar và là Phó Giám đốc Phòng thí nghiệm Khoa học Máy tính và Trí tuệ Nhân tạo. Nghiên cứu của ông chủ yếu tập trung vào mô hình hóa và thiết kế phần mềm. Ông là người tạo ra ngôn ngữ mô hình Alloy và là tác giả của Tóm tắt phần mềm: Logic, Ngôn ngữ và Phân tích (MIT Press; xuất bản lần thứ hai năm 2012). Nhận được Giải thưởng Tác động ACM SIGSOFT năm 2016 , Giải thưởng Nghiên cứu xuất sắc ACM SIGSOFT năm 2017, và là Thành viên ACM.

Uri Kolodny: Đồng sáng lập kiêm Giám đốc điều hành tại StarkWare , đồng thời là thành viên Hội đồng quản trị của công ty. Anh ấy có bằng Cử nhân về CS của Đại học Hebrew, và bằng Thạc sĩ Quản trị Kinh doanh của MIT Sloan. Uri là một doanh nhân nối tiếp, người đã đồng sáng lập một số công ty công nghệ, trong số đó có OmniGuide (một công ty MIT phát triển sợi quang học cho phẫu thuật nội soi) và Mondria (nhà phát triển các công cụ trực quan hóa dữ liệu lớn). Trước đây, Uri cũng từng là EIR với hai công ty VC của Israel và là nhà phân tích tại McKinsey.

Stani Kulechov: Người sáng lập kiêm Giám đốc điều hành của Aave Protocol, một Công ty khởi nghiệp Blockchain hàng đầu về cho vay phi tập trung. Stani cũng là một nhà đầu tư và cố vấn của nhiều giao thức hàng đầu và mang tầm nhìn của mình để định hình tương lai và việc áp dụng các Ứng dụng Tài chính Phi tập trung. Ông có bằng Thạc sĩ Luật tại Đại học Helsinki. Stani đang giúp Certora phát triển kinh doanh.

Avihu Levy: Bằng Cử nhân về EE và Vật lý từ Technion. Ông có 8 năm kinh nghiệm trong lĩnh vực nghiên cứu bảo mật các giao thức mạng và thiết bị di động. Avihu là một người đam mê blockchain và đã làm việc trong một số dự án trong lĩnh vực này, bao gồm đồng sáng lập một công ty khởi nghiệp kinh doanh tiền điện tử. Avihu là trưởng bộ phận sản phẩm của StarkWare.

Simon Morris: Nhà tư vấn và điều hành công nghệ dày dạn với hơn 20 năm kinh nghiệm tại Thung lũng Silicon và có kiến thức sâu rộng về các công nghệ phi tập trung và không gian ngang hàng. Ông đã làm việc gần 10 năm tại BitTorrent Inc với nhiều vai trò bao gồm Giám đốc chiến lược và Tổng giám đốc. Ông đã lãnh đạo việc thiết kế cái được gọi là công nghệ mã thông báo BTT của BitTorrent và đóng một vai trò quan trọng trong việc bán công ty sau đó. Ông có bằng MBA tại Trường Kinh doanh Sau đại học Đại học Stanford và các bằng MPhil và BA / MA về Chính trị và Kinh tế của Đại học Cambridge.

Moti Rafalin: Giám đốc điều hành và doanh nhân phần mềm với hơn 20 năm kinh nghiệm trong thị trường phần mềm nhập khẩu, tập trung vào cơ sở hạ tầng và bảo mật. Người đồng sáng lập và Giám đốc điều hành tại vFunction, hiện đang ở chế độ ẩn và của WatchDox đã được BlackBerry mua lại. Trước khi đồng sáng lập WatchDox, là Tổng Giám đốc Kinh doanh Quản lý Ứng dụng tại EMC. Tốt nghiệp Technion, Học viện Công nghệ Israel (Summa kiêm laude), và có bằng MBA của Trường Kinh doanh Harvard.

GS Noam Rinetzky: Chuyên gia về xác minh chính thức, ngôn ngữ lập trình, hệ thống đồng thời và phân tán. Ông đã phát triển các yêu cầu về tính đúng đắn cốt lõi để kiểm soát đồng thời. Ông nhận bằng Tiến sĩ khoa học máy tính tại Đại học Tel Aviv. Noam là người nhận được học bổng IBM danh giá cho các nghiên cứu Tiến sĩ của mình và Học viện Kỹ thuật Hoàng gia / Nghiên cứu EPSRC cho các nghiên cứu sau tiến sĩ.

Công nghệ

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.

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

Tài chính

Certora đã huy động tài trợ vòng series A với tổng cộng 7.2 triệu đô la Mỹ từ các Nhà đầu tư: A.Capital Ventures, Semantic Ventures, VMware, Coinbase Ventures, Electric Capital, và nhiều nhà đầu tư thiên thần khác.

Sản phẩm

Certora cung cấp 2 giải pháp cho người dùng

Xác minh chính thức 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 an toàn 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 đề mới 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.

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.

Đố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.

Đối tác

Đối tác là các quỹ lớn: A.Capital Ventures, Semantic Ventures, VMware, Coinbase Ventures, Electric Capital, .

Các khách hàng của Certora: Coinbase, Compound Finance, Celo, Orchid, AAVE, Opyn, TBTC, Balancer, Synthentix, Origin, Dforce, Sushiswap, Furucombo, Syndicate, Maker, Notional, Rolla, Paraswap, Indexed Finance, BenQi, Orca, OpenZeppelin. ..

Tokenomics

Đang cập nhật

Cộng đồng

Mua Certora ở đâu?

Certora chưa được niêm yết trên bất kì sàn giao dịch nào. GFS Blockchain sẽ cập nhật thông tin khi có thông báo list sàn.

Kết luận

Certora là có công nghệ Prover để đảm bảo bảo mật của hợp đồng thông minh; xác minh chính thức tạo ra bằng chứng rằng một phần mềm đáp ứng một đặc điểm kỹ thuật

Certora hiện đang phân tích mã byte EVM kết hợp hai kỹ thuật khoa học máy tính: giải thích trừu tượng và giải quyết ràng buộc.

Hy vọng với những thông tin trên sẽ giúp các bạn có cái nhìn tổng quan về Certora. GFS Blockchain sẽ liên tục cập nhật thông tin mới về thị trường, mọi người hãy theo dõi thường xuyên chuyên mục thông tin dự án tại website và đừng quên tham gia vào nhóm cộng đồng của GFS để cùng thảo luận, trao đổi kiến thức và kinh nghiệm với các thành viên khác nhé.