Post
Topic
Board Announcements (Altcoins)
Topic OP
ANN [Kripke] Provably secure contracts; functional language; on-chain encryption
by
KripkeSecure
on 08/08/2016, 12:31:23 UTC
Launch date TBC

//




kripke


n  |  “cryp-key”  |  \ krip-kē \



We* introduce Kripke, an exploration of "rigid designation" in the context of blockchain insecurity (specifically, malleability).


Problem description:
Smart contracts on Ethereum cannot be proven to be trustless. The Turing-completeness of Ethereum's scripting language makes it impossible to prove that a statement written in Solidity always returns the same result. Insecurity is a permanent feature of Solidity and any Turing-complete language.
We contrast this with Saul Kripke's notion of a "rigid designator," introduced in Naming and Necessity (1972):

A rigid designator designates the same object in all possible worlds in which that object exists and never designates anything else.


Intuitively, for smart contracts, rigid designation implies that a contract must be interpreted in exactly one way. As such, it completely avoids the insecurities of Bitcoin's malleability and Ethereum's inability to ensure determinate outcomes to contracts written in Solidity.



Thus we define the following features of Kripke-secure blockchains:


kripke-security

Kripke-security denotes security by virtue of determinacy of outcome. A statement in a given language is Kripke-secure if it designates rigidly, that is, it has exactly one meaning for all possible worlds.

A candidate technique for achieving Kripke-security is formal verification of (purely) functional language.


kripke-function

A Kripke-function has the same outcome in all possible worlds in which its semantics exist and never has any other outcome.

Obvious candidates for implementing Kripke-functions are functional languages (Haskell; Scala) with suitable type systems.


kripke-keystore

A Kripke-keystore is a system of Kripke-functions for the implementation of an encryption key storage facility on-chain.


kripke-contract

A Kripke-contract utilises only Kripke-functions, thus determining an entirely non-malleable outcome.


kripke-governance
Kripke-governance utilises only Kripke-contracts to determine provably trustless outcomes of social decisions, like voting or allocating funds.


//


coin specification

Concurrent POW/POS implementation
POW consensus algorithm: SHA256
Block time: ~10 minutes
Block reward to decrease in inverse proportion to difficulty
POS coin age maturation: 24 hours
Annual POS interest: 4%
Premine: 10 million, held by Foundation for ITO sale



project phases

Phase 1
Launch date: 20 Aug 2016
Blockchain inception
Mining begins
ICO funds mined at genesis block
Temporary use of stock PPC clone

Phase 2
ICO commences
Sale of 10 million tokens
Minimum amount to proceed to Phase 3: 2000 BTC

Phase 3
Kripke-secure development begins
Broad-based community collaboration, via Foundation contracts
Foundation to retain a portion of unsold ICO tokens to fund development (disbursed via contract)


references
http://langsec.org/    
https://en.wikipedia.org/wiki/Formal_methods    
http://plato.stanford.edu/entries/rigid-designators/    
http://plato.stanford.edu/entries/possible-worlds/
https://en.wikipedia.org/wiki/Chomsky_hierarchy


*Due to the experimental nature of this project, and due to its potential to impact upon our public identities and employment, we choose to remain anonymous for the time being.


Please note: this project is strictly experimental in nature and is not "currency" or "property". Additionally, the project may fail, or fail to attract sufficient support. Its purpose is solely to explore the potential of rigid designation to secure smart contracts.