Safety and Liveness
The concepts of safety and liveness are fundamental to the design and operation of decentralized systems, particularly in the context of smart contracts and bridging mechanisms like those employed by BitVM. This article delves into the nuances of these properties as they pertain to BitVM's smart contract architecture and its derivative, the BitVM Bridge. By exploring both the deployment and operational stages of BitVM smart contracts, we aim to provide a comprehensive understanding of how these systems ensure security and reliability while maintaining operational continuity.
Safety and Liveness in BitVM Smart Contracts
BitVM smart contracts operate through two distinct stages: the deployment stage and the running stage. At the deployment stage, a transaction graph is created and presigned by a committee of participants, while the running stage involves participants executing actions in accordance with the predefined transaction graph. These stages form the foundation for evaluating both safety and liveness in the system.
Safety
Safety Assumptions
The safety of BitVM smart contracts hinges on specific assumptions tied to each stage of the contract lifecycle. During the deployment stage, all operations occur off-chain, making safety considerations largely irrelevant at this point. However, at the running stage, safety is critically dependent on the behavior of the attesters. Specifically, if at least one attester deletes their signing key after the deployment stage, the contract remains secure and resistant to manipulation. This key deletion ensures that no unauthorized modifications can occur, preserving the integrity of the transaction graph.
Safety of the Attesting Procedure
The attesting procedure, a cornerstone of the deployment stage, leverages the MuSig2 algorithm to ensure cryptographic integrity. The MuSig2 algorithm guarantees that all honest attesters produce the same signature, denoted as , for a given message. This uniformity arises from the synchronous network assumption, which ensures that all attesters receive the same set of partial signatures, , within a bounded time . Consequently, if an honest attester outputs a valid signature , it is inevitable that all other honest attesters will do the same.
Moreover, the protocol ensures that malicious attesters cannot generate a valid signature for an invalid message . For a valid signature to exist, all attesters would need to contribute partial signatures , including at least one from an honest participant. However, an honest node will categorically refuse to generate a partial signature for an invalid message, thereby preventing the creation of . This property is crucial in maintaining the integrity of the attesting procedure and ensuring the system's overall safety.