Design and Formalization of Blockchain Oracles By: Mohammad Shaheer Advisor: Giselle Reis • Blockchain: Decentralized, distributed ledger that stores information securely and transparently. • Ethereum: Blockchain based decentralized computing platform that allows developers to build dApps (Decentralized Applications). • Smart Contracts: Computer programs running on Ethereum that can be called by users by creating requests. • Example: Alice agrees to pay Bob X ETH if team Y wins the match. The smart contract for this match needs to obtain the results of the match. • Solution 1: Smart Contracts call the off-chain APIs themselves. Issue: Blockchain loses determinism. • Solution 2: Oracles Entities that connect blockchains to external systems 1. Background • Oracle Problem: Connecting Blockchain to off-chain systems without losing the transparency, consensus and decentralization. • Agood oracle should satisfy the following properties: 1.Confidentiality, Integrity and Availability 2.End-to-End Decentralization 3.Discourage Dishonest Behavior • Problems with current oracles: 1. No formal guarantees 2. Ad hoc 3. Prone to attacks by malicious entities 4. Uncertainty 2. Problem • Chainlink is the most trusted Oracle used in industry. • Adopts decentralization at every layer. • Issues: 1. Not Formally Verified 2.Complex Implementation 3. State of the Art • Provide guarantees through Formal Verification. • Ensure protocol is sustainable and charges consumers fairly. 4. Our Approach • Smart Contract implemented using Solidity. • Every external data source connected to an oracle smart contract on- chain. • Data Model: Subscription based model. Consumers deposit credit to obtain data. • Price setting Model: 1. Every consumer charged (weight * base fee). 2. The model tries to keep the total cost and total revenue the same by adjusting the Base Fee at periodic intervals. 3. 𝑹𝒌+ 𝝓′ ∗𝛀𝒌= 𝑪𝒌+ 𝜶𝒌∗𝑵𝒌(Solving for 𝜙′). • Under certain assumptions, total cost equals total revenue right before the next base fee adjustment. 5. Implementation • Coq (Interactive Theorem Prover) used for formalizing the Solidity smart contract. • The oracle is modeled as a state machine. • The state of oracle is formalized as an n-tuple. • Trace: Record of events ordered from least-recent to most-recent. • Using the initial oracle state and the trace we can track the evolution of the oracle state. 6. Formalization 𝑆𝑡𝑎𝑡𝑒𝑖+ 𝑃𝑎𝑟𝑎𝑚𝑒𝑡𝑒𝑟𝑠 𝐶𝑜𝑞𝐹𝑢𝑛𝑐𝑡𝑖𝑜𝑛 𝑆𝑡𝑎𝑡𝑒𝑖+1 • Theorem 1: After every action, the credit of all consumers remains non- negative. 2 helper lemmas • Theorem 2: Between any 2 data write calls, a consumer pays exactly once for obtaining data. 9 helper lemmas • Theorem 3: If the base fee is adjusted under certain assumptions, total revenue equals total cost right before the next base fee adjustment. 16 helper lemmas • Theorems proved inductively using the trace. • Desired property and assumptions expressed as Coq propositions. 7. Specifications • PID Control: Technique used in Control Theory to control the system’s behavior (controlled variable) in order to achieve the desired output (commanded variable). • Intuitively, it’s a function that receives an input and produces an output. • Objective: Over time, we want the total revenue (controlled variable) to be equal to the total cost (commanded variable) which indicates sustainability and fairness of the protocol. 8. Price Setting using PID control Total Cost Total Revenue Base Fee • We can modify the Adjust Base Fee function to implement a PID control. • Determining 𝑲𝒑,𝑲𝒊,𝑲𝒅(also known as gains) is the main challenge. • Heuristic Approach: Run input sequences and use Cohen Coon/Ziegler Nichols method for determining the gains. • Model Based Approach: Determine a model that describes how the total revenue is affected by the base fee and use it to determine gain values. • 𝑻𝒐𝒕𝒂𝒍𝑹𝒆𝒗𝒆𝒏𝒖𝒆𝒕= ׬𝟎 𝒕𝝓𝒕∗𝒓𝒕𝒅𝒕 • 𝑻𝒐𝒕𝒂𝒍𝑪𝒐𝒔𝒕𝒕= ׬𝟎 𝒕𝜶𝒕∗𝒘𝒕𝒅𝒕 Total Revenue = 𝑅𝑘 Total Cost = 𝐶𝑘 Reads = Ω𝑘 Writes = 𝑁𝑘 Latest Cost = 𝛼𝑘 Base Fee Adjustedk Total Re