> How would such a proof checker know the intent of the code of not having backdoor/insecurity? How do you define security in a logical sense?
As you surely know, there is no such thing as secure/insecure, but a set of properties that are considered in IT security, which might even not be fullfillable all at the same time. The exact words vary depending on the book, but a popular classification in a German standard reference on IT Security is
General protection goals:
- Integrity
- Confidentiality
- Availability
Further goals are
- Authenticity
- Acountability
- Non Repudiation
- Sometimes Anonymity
So you first begin to formulate your protection goals. Next you can begin to forumulate this in a logical sense. Again there can exist quite different axiomatic implementations of a general protection goal.
There's a lot of work in CompSci on this that predates all the blockchain-related stuff. They usually call it "security-typed languages" or "information flow security." Here's a paper with a lot of prior work in that plus an example tool and language:
The main assumption is that the specification (the proposition you want to prove) is (much) simpler than the proof. This means that the user/customer can read the specification, and understand what it means, even if the proof is not comprehensible to them. Of course, the proof must then be machine-checkable.
This makes the clarify of specifications into a market-driven problem. What do you do if you have a formally proven contract, but nobody can understand what the spec is? Well, you probably won't be able to sell it, because nobody will trust you. Instead, you try to simplify the specification, so you have something that people will trust. This is very similar to established practice of mathematics, where getting a proof accepted is really a social process, in which you try to convince your fellow mathematicians that the proof is correct.
How would such a proof checker know the intent of the code of not having backdoor/insecurity? How do you define security in a logical sense?