Roadmap Formal Verification

Automatically Derived High-level Properties Original to Glow

• Balance: The amount in sub-accounts of an interaction at the end of the interaction is 0.
• Non-negativity: Amounts of assets in any account or sub-account are always non-negative.
• No Overflow: Integer operations never overflow on the happy path, and inputs that might cause overflow are trapped rather than left to cause unhappy behavior.
• Linearity: Assets cannot be created or destroyed or duplicated or divided, only added via explicit deposits, removed via explicit deposits or transferred between accounts.
• Liveness: Within the participants' respective explicit economic hypotheses, a/the optimal strategy for each participant is to keep executing his program.
• Safety: Within each participant's explicit economic hypotheses, whatever the actions of other participants, the participant's wallet will keep its value, except for the payment of transaction fees, which is bounded in gas.
• Termination: Interactions always reach the end; servers complete all their requests and reach back the request loop.
• Mutual profit, rather than fairness: Given probabilistic expectations of costs and benefits in each participant's model, even accounting for fixed gas cost and fixed loss of opportunity for the capital, then, if the user's valuation verifies suitable hypotheses (to be made explicit to the user), the user will profit from using the DApp if the other users cooperate, which they are also interested in doing if their valuations verify the suitable complementary hypotheses (e.g. seller vs buyer has opposite utility functions for the given quantity of cash vs the item sold). At the very least, each participant must receive something out of the interaction, or else its incentive structures are wrong and some participant can be expected to defect.
• Cooperation: Formally verify the difference between cooperative flows that can use state channels and adversarial flows that must use a censorship-resistant blockchain (or side chain market, if a single operator can be adversarial).
• We must document what exactly we verify.

These ought to be consequences of the above already:

• No withdrawal during the first transaction, or the recipient got something for nothing, that the first participant loses.

Logic Model for User-Defined High-level Properties Original to Glow

The programmer may specify additional application-dependent invariants of his own to the interaction.

• Concurrent Tree Logic
• Epistemic Logic
• Linear Logic for resources
• Game Semantics
• Game Theory
• Distinct notions for Liveness and Safety assertions: just choice of top-level quantifiers?
• Document the precise semantics of our logic
• Generate counter-examples as testing scenarios for proofs of no liveness or no safety

Low-level properties like competition

• No arithmetic overflow / underflow.
• No gas attack wherein someone can prevent completion of some actions.
• No gas attack wherein someone can increase gas costs for others.
• Verify high-level state machine semantics is preserved at the low-level (Full abstraction?).
• Verify that interactions always terminate.
• Verify that libraries can't be deleted.
• Prevent cyclic dependencies between transactions.
• Prevent bad behavior from reentrancy.
• Ensure that transactions are guarded by the proper access control
• Atomicity of compound transactions
• Balance preservation: resources behave linearly, aren't created or destroyed outside specific events.
• Cheat-resistance: there isn't a backdoor allowing someone to grab more than accounted for in the application model.
• Liquidity: you can always take your money away.
• Fairness: all contract participants have the opportunity to participate
• Stability within economic hypotheses: if the prices remain within input range, no participant can extract or lose value outside output range (Not resistant to someone who can predict future fluctuations outside the assumed range.)

Low-level properties better than competition

• Compute worst case execution times, gas expenses.
• Compute maximum allowed parameter sizes.