ball_nebula

Axiom Principle_of_Explosion : forall P Q:Prop, P /\ ~ P -> Q.

From Contradiction, Anything Follows.

secbit
FORMALIZING A SECURE BIT WORLD
STARTING FROM FORMALIZING SMART CONTRACTS

PLATFORM FOR SMART CONTRACT SECURITY

The security of smart contracts is of great importance to a healthy Ethereum ecosystem. However, it is not a trivial task to develop secure smart contacts using languages such as Solidity, due to their inherent issues and vulnerabilities. We present SECBIT, a framework that could fundamentally change smart contract security landscape. Backed by the full strength of formal specifications and mathematical proofs, SECBIT incorporates three levels of auditing services to address all aspects of security issues in smart contracts.
animate1_08.png animate1_09.png
animate1_05.png animate1_06.png animate1_07.png

SEMI-AUTOMATED VERIFICATION

The first level of SECBIT is a semi-automatic verification service that identifies common issues and vulnerabilities in smart contracts. This is done using state-of-the-art automatic formal analysis tools, in combination with manual triaging based on our expert understanding of the intention and implementation of the contract-under-auditing. The findings are provided in a detailed source-code-level security auditing report with remediation advises.
animate1_09.png
animate1_09.png
animate1_09.png animate1_09.png animate1_09.png

FURTHER VERIFICATION WITH FORMAL SPECIFICATION

This service extends our first level of offering with a customized process to formalize the requirement and logic of a contract with our innovative formal specification language. The process not only provides a rigorous examination of the contract to reveal deep logical defects, but also helps to guide our tools to conduct more accurate verification, resulting in a higher-level of assurance in the findings provided in the auditing report.

All instances of smart contract theft or loss – in fact, the very definition of smart contract theft or loss, is fundamentally about differences between implementation and intent.

- Vitalik Buterin

FULL FORMAL VERIFICATION

Our highest level of service consists of a complete formalization of a smart contract in our specification language, as well as a formal security proof at instruction-level with minimal Trusted Computing Base and maximal assurance. Advanced smart contract properties, such as fairness, would also be proven using techniques from Game Theory, such as proving the existence of a Nash equilibria. The result of this service would be a EAL7-level security auditing report.
animate1_09 animate1_09 animate1_09