We are the only team which provides
Prover technology for checking security rules with the following features:
Reported errors are real
For proven rules, no missed alarms
No need for human intervention
Supports arbitrary programs and integrates into CI/CD pipeline
Static Asset Scanner: A monitor layer for smart contracts providing up to the minute security of the bytecode.
Quality Development Environment: A CD/CI platform for smart contract development.
Certora provides security analysis tools for Smart Contracts. Certora has unique technology called Certora Prover capable of checking at compile-time that all executions of a Smart Contract fulfill a set of security rules.
Certora Prover technology is available as a tool that complements existing compilers and debuggers of Smart Contracts. It checks that the contracts adheres to the interface requirements of other contracts. Certora’s blockchain independent and language-agnostic Prover technology precisely identifies bugs in Smart Contracts and proves their absence. Certora offers two unique solutions targeted for all participants in the blockchain ecosystem:
Static Asset Scanner
(SAS) for businesses that employ Smart Contracts. We currrently check ERC standards.
For each scanned contract, we report the security rules that it obeys and provide inputs demonstrating violated rules.
SAS guarantees long-term safety of your digital assets in the blockchain by notifying immediately on any new issues, thus reducing incident response time. This allows your business to avoid the consequences of undesired irreversible transactions.
Quality Development Environment
(QDE) for developers is a CI/CD plugin that allows developers to move fast and break nothing.
Developers can detect issues during development,
assist in QA,
and maximize security before contract deployment.
QDE automatically produces a report of existing issues, reporting their severity and the exact manner in which they reproduce, integrating seamlessly into existing CI/CD pipeline.
Our first post explains Why testing is not enough for million-dollar code.
Coinbase is a leading digital currency exchange based in San Francisco, providing professional and consumer grade trading products allowing users to buy, sell, send, and receive most major digital assets.
Compound is a transparent, autonomous money market — allowing users & applications to frictionlessly earn interest or borrow Ethereum assets without relying on a counterparty.
Celo is an open platform that makes financial tools accessible to anyone with a mobile phone.
Orchid is a decentralized virtual private network (VPN), allowing users to buy bandwidth from a global pool of service providers.
StarkWare solves the inherent problems of blockchains - scalability and privacy. It develops a full-proof stack, using the STARK technology to generate and verify proofs of computational integrity. StarkWare's cryptographic proofs are zero-knowledge, succinct, transparent and post-quantum secure. It's first product is a STARK-based scalability engine powering non-custodial crypto exchanges.
Certora Prover builds on 30 years of academic research and hundreds of academic publications which pioneeered the area of Formal Verification. The team combines academic leadership, industrial strength and Blockchain expertise.
Nurit holds a PhD from Tel Aviv University in Static Code Analysis. She is an author of 13 academic papers and 35 patents. She was a CSO at Panaya, a static-analysis company acquired by Infosys and a research manager at KayHut. Nurit has extensive experience in static and dynamic analysis of low-level bytecode. Hands-on experience in transferring ideas from research to robust products.
Anastasia is a software engineer finishing her B.Sc. in Computer Science and Economics at Tel-Aviv University.
Blockchain enthusiast with background in Formal Verification. She is also an experienced software engineer which spent 5 years at Check Point. Shelly is the lead author of the isolation technique for ensuring the correctness of modular reasoning. She graduated from the Adi Lautman undergraduate excellence program and is a PhD candidate in Smart Contract Verification at Tel Aviv University.
Professor and a Chair of Software Systems in the School of Computer Science at Tel-Aviv University with 30 years of experience in formal methods and static code analysis. He contributed techniques which were integrated into the Microsoft device driver verification tool and Panaya ERP tool acquired by Infosys. He is also a co-designer of Ivy. He a fellow of ACM and a recipient of Microsoft Outstanding Award for contributions to formal methods. Sagiv is a recipient of the most prestigious European grant. He has more than 200 academic publications with Google H-index 55.
Experienced software engineer with rich practical experience in software systems development at Elite Technological IDF Unit, Google and at Dell EMC. Acted as team leader and core team architect. He is the lead author behind the technique for modularly verifying distributed systems integrated into Ivy. He holds bachelor in Computer Science Cum Laude from the Technion Israel Institute of Technology
Dr. James Wilcox recieved his PhD. in June 2019 from the University of Washington. Dr. Wilcox is the architect of a system called Verdi for formally verifying distributed systems. He is an author of 15 academic papers. He is enthusiastic to make formal verification real.
Thomas is finishing his Bachelor's Degree in Computer Science at the University of Washington. He has focused on Programming Languages and Formal Methods through his academic career and every day enjoys the opportunity to apply this knowledge to solving problems with Certora.
Lior is a security researcher with over 6 years of experience in the vulnerability and exploitation fields. In his spare time, Lior is also an MSc. student for physics at the Weizmann Institute.
Alexander likes logic. He did his PhD research all over the areas of program verification, static analysis and SMT. He published several research papers and is one of the main developers of the award-winning program verification tools of the Ultimate framework (e.g. Ultimate Automizer, Kojak, TreeAutomizer, Unihorn Automizer). He also worked on the interpolating SMT-solver SMTInterpol.
Or holds a BSc in Computer Science, Cum Laude, from Tel Aviv University. He received his MSc in Computer Science from Tel Aviv University in 2019. His research focuses on automated synthesis of reactive systems from specifications, specifically, making this technology useful for software engineers. He is one of the developers of Spectra, a specification language and tools for reactive synthesis. He has co-authored several research papers that tackle the challenge of enriching the specification language while still maintaining synthesis scalable.
Dr. John Toman received his PhD in 2019 from the University of Washington. Dr. Toman's research focuses on bringing the power of automated verification to real world, industrial settings. His award-winning, impact focused research has been published in several top conferences in the field.
Alex is the Alcatel-Lucent Professor of Computer Science at Stanford. Alex received his Bachelors degree in Computer Science and Music from Bowling Green State University in 1983 and his Ph.D. from Cornell University in 1988. Alex was a Research Staff Member at the IBM Almaden Research Center (1988-1993) and a Professor in the EECS department at UC Berkeley (1993-2003) before joining the Stanford faculty in 2003. His research interest is in areas related to programming languages. He is an ACM Fellow, a recipient of Phi Beta Kappa's Teaching Award, and a former chair of the Stanford Computer Science Department (2014-18).
Jeff Flowers interests in computers began with the realization of the power of open and private communication in the early 90s with the release of PGP. From this initial spark demonstrating how applied cryptography could empower the individual to then seeing these techniques used to create novel global communication networks, he has continued his exploration of these powerful tools. He was Director of Curriculum and Instruction at Blockchain University and continues to lecture at DLT Education on the emerging field of Blockchains. At Certora Jeff provides a lens crafted from the numerous Blockchain and DLT based projects he is associated with, as well as being an active member of multiple technology focused communities around Silicon Valley. When he is not working on these endeavors, Jeff is a tenured Professor at the College of San Mateo's Math Sciences Division teaching Chemistry. His doctoral work, at San Francisco State University, focused on the use of neural networks and gamification protocols towards the optimization of educational pathways.
Yona is a seasoned industry expert and entrepreneur, he has over 20 years of management and technology experience in the cyber security space. Yona was a co-founder of Fortsacle in the area of User Behavioral Analysis (UBA) which was acquired by RSA at 2018. Prior to founding Fortscale, he founded and managed Cyber Security, a boutique technology consulting firm. Yona also was a founder and served as VP of Security Research at Entercept, which was acquired by McAfee in 2003 for $120M. Yona then continued as VP of Security Research at McAfee HQ in Santa Clara. Before that, he worked as VP of Business Development at Netect, a pioneer in vulnerability assessment technology, which was acquired by BindView in 1999. Yona holds a PhD. in Computer Science from the Israel Institute of Technology (Technicon).
Immerman is a renowned computer scientist studying logic in computer science and descriptive complexity. He received B.S. and M.S. degrees from Yale University in 1974 and his Ph.D. from Cornell University in 1980. His book Descriptive Complexity appeared in 1999. He received a Göedel Prize for solving a 20 year open problem in computer science theory. Immerman is an ACM Fellow and a Guggenheim Fellow.
Daniel Jackson is a Professor of Computer Science at MIT, a MacVicar teaching fellow, and an Associate Director of the Computer Science and Artificial Intelligence Laboratory. His research has focused primarily on software modeling and design. He was the creator of the Alloy modeling language, and author of Software Abstractions: Logic, Language, and Analysis (MIT Press; second ed. 2012). His current research projects include development of new paradigms for end-user programming, a safety interlock for self-driving cars, and a new theory of software design that connects user experience to essential conceptual structures. He was a recipient of the 2016 ACM SIGSOFT Impact Award, the 2017 ACM SIGSOFT Outstanding Research Award, and is an ACM Fellow. Jackson is also a photographer; his most recent project is Portraits of Resilience.
Uri is a co-founder and CEO at StarkWare, and a member of its Board of Directors. He has a BSc (Magna cum Laude) in CS from the Hebrew University, and an MBA from MIT Sloan. Uri is a serial entrepreneur, who has co-founded several technology companies, among them OmniGuide (an MIT spinoff developing optical fibers for endoscopic surgery), and Mondria (developer of tools for visualization of big data). Previously, Uri also served as an EIR with two Israeli VC firms, and as an analyst at McKinsey.
Avihu has a BSc (Summa cum Laude) in EE and Physics from the Technion. He has 8 years of experience in security research of network protocols and mobile devices. Avihu is a blockchain enthusiast, and has worked on several projects in the field, including co-founding a cryptocurrencies algo-trading startup. Avihu is the head of product at StarkWare.
Simon is seasoned technology executive and consultant with over 20 years experience in Silicon Valley and a deep knowledge of decentralized technologies and the peer-to-peer space. He worked for almost 10 years at BitTorrent Inc in many roles including Chief Strategy Officer and General Manager. He led the design of what became known as BitTorrent's BTT token technology and played a key role in the subsequent sale of the company. He holds an MBA from Stanford University Graduate School of Business and MPhil and BA/MA degrees in Politics and Economics from Cambridge University.
Software executive and entrepreneur with over 20 years of experience in the enterprize software market with a focus on infrastructure and security. Co-founder and CEO at vFunction, currently in stealth mode, and of WatchDox which was acquired by BlackBerry. Before co-founding WatchDox, was the General Manager of the Application Management Business at EMC. A graduate of the Technion, Israel Institute of Technology (Summa cum laude), and holds an MBA from the Harvard Business School.
Noam Rinetzkey is an expert in formal verification, programming languages, concurrent and distributed systems. He developed core correctness requirements for concurrency control. He received a PhD in computer science from Tel Aviv University. Noam is a recipient of the prestigious IBM scholarship for his PhD studies and Royal Academy of Engineering/EPSRC Research for postdoctoral studies.
Yes. There are actually two difficult problems:
(1) How does one define what requirement to check
(2) Given a requirement, how to make sure that all executions of the program fulfill the requirement. The Certora proprietary technology, Certora Prover, addresses the second problem. The second problem is especially interesting for software systems such as Smart Contracts, in which the number of potential states is infinite. This is realized in programs with loops and contracts which call each other. In fact, virtually all contracts have an infinite state since they are reactive.
Therefore, we develop unique technology which can reason about such programs in an accurate way.
Certora offers two mechanisms:
(1) A list of predefined requirements based on best practices defined by the Smart Contract community.
(2) The user defines requirements using a new command called 'ensures' which behaves similarly to Solidity's assert, but is checked at compile-time by the Certora Prover engine.
Certora optionally enforces a requirement which ensures that external contracts cannot change the internal state of the checked contract. This automatically prevents bugs like the DAO. It also enables Certora Prover to verify the code without considering the potentially complicated code of the external contract. Thus, Certora verifies one contract at a time. In the formal method community this is called rely-guarantee reasoning. This is similar to the notion of separate compilation in compilers.
Certora facilitates trust by the combination of the following:
(1) Providing an executable tool where users can review the verification process and reproduce it at any point in time.
(2) Generating artifacts of the verification, which can be reviewed by non-experts without depending on Certora's tools. These artifacts are test inputs that demonstrate pathes in the code which lead to violations and satisfaction of requirements.
(3) Developing proprietary technology for automatically generating machine checkable proofs. In Computer Science, this area is called Proof-carrying code.
Smart contracts are vulnerable to so called "callback attacks".
The attacker contract can exploit the fact that the internal state of the
contract is not yet stable.
This happened in the
DAO attack and the
One way to avoid the problem is to limit the use of callbacks to occur in the last
command in the contract but this can be too restrictive in many cases.
Effectively Callback Freedom: We are enforcing a requirement which permits liberal usage of callbacks as long as the state of the contract cannot be manipulated in a way which breaks its correctness. For additional documentation, refer to:
- A short Video by Shelly Grossman
- A long Video by Noam Rinetzky taken at POPL'18 LA
- Academic Paper
- Technical Report
Acknowledgements This is a joint work between Vmware Research Group, Tel Aviv University and Stanford University.