ANN [Kripke] Provably secure contracts; functional language; on-chain encryption - page 2.

KripkeSecure

newbie

Activity: 13

Merit: 0

Quote from: PGPpfKkx on August 08, 2016, 08:16:42 AM

min 2000BTC + anonymous? oh yeah Roll Eyes

anonymous because of experimental nature? Care to expand this thought a bit?

We've seen many developers try something, have sentiment turn against them, and find their reputations wrecked.
This is in addition, and separate from, the possibility that this project could fail.
Finally we have real-world commitments that would be impacted by the sorts of knock-on effects that this community can cause.

Our value proposition is:
* we wanna do something to contribute to smart contract security.
* we have strong reasons to not trust Bitcointalk with our reputations.
* to do what's planned will take a lot of work. Having enough funding is necessary for the success of the project.
* we think we can give smart contracts in general, for the foreseeable future a means of being provably secure.
* this is your chance to be first to market with this tech.

(FYI we're not here to discuss this further. Take it or leave it.)

PGPpfKkx

hero member

Activity: 586

Merit: 501

min 2000BTC + anonymous? oh yeah Roll Eyes

anonymous because of experimental nature? Care to expand this thought a bit?

KripkeSecure

newbie

Activity: 13

Merit: 0

Quote from: LazurusBehold on August 08, 2016, 07:37:16 AM

The Big Bang Theory's Kwipki ? Tongue

Kripke with rhotacism? ;-)

Either way, it's this guy:

https://media1.britannica.com/eb-media/37/99637-004-E8C87E5E.jpg

RidgyDidge

sr. member

Activity: 369

Merit: 250

Quote from: LazurusBehold on August 08, 2016, 07:37:16 AM

The Big Bang Theory's Kwipki ? Tongue

My Initial thoughts too.... wheres that wabbit Grin

celot

sr. member

Activity: 1492

Merit: 269

ICO again?

LazurusBehold

newbie

Activity: 45

Merit: 0

The Big Bang Theory's Kwipki ? Tongue

KripkeSecure

newbie

Activity: 13

Merit: 0

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.

Topic: ANN [Kripke] Provably secure contracts; functional language; on-chain encryption - page 2. (Read 2111 times)