author: aman
Blog III - Part III - Day 13
Understanding Hyperproperties and Blockchain together. And how this could be so big!
Let’s get in….
In this micro-blog
- Let us check this vaguely
- 2-trace property
- Hyperproperties
- Safety and Liveness - Another 2 very Important terms
- Blockchain & Hyperproperties
- How this could be so big?
Safety and Liveness - Another 2 very Important terms
As already explained, Property is a set of traces(traces are the set of System states). So, intuitively the Properties are the set of all the traces, where the system can reach.
Now, there are two things to be well noted, there are certain states “where a system should never reach & certain states where a system should eventually reach.
Well these are termed as “Safety” and “Liveness” trace properties. Where: Safety: is the property that prescribes that a system should never reach some bad state , while Livenes: is the property that prescribes that a system shoudl “eventually” reach some “Good State”.
Give some time understanding this stuff. These are 2 very important terms when thinking about System proofs.
Every trace property is an intersection of safety & liveness property.
Blockchain & Hyperproperties
A very straight explanation from Hyperpoperties paper[1], says
“If systems are modeled as sets of execution traces [35], then the extension of a system property is a set of sets of traces or, equivalently, a set of trace properties. We name this type of set a hyperproperty.”
Thus these safety and liveness property are said as heypersafety & hyperliveness.
Every property of any system anywhere can be defined in terms of these hyperproperties…
Now you must remember there was a CIA triangle, that Hrishabh explained about in Winter School 2019, which stands for : (take an example of something stored inside a locker)
| C -> Confidentiality | can’t see what is inside the locker |
|---|---|
| I -> Integrity | can’t tamper what is inside the locker |
| A -> Availability | can’t destroy the locker’s availability |
If you think very crucially, you’ll find that only confidentiality and intergrity are the two properties concerned with the secure information flow.
The most invincible idea behind blockchain is the safety of data.
To ensure the flow of data never goes in wrong hands, which is described by the very term secure information flow.
Now considering application of hyperproperties in the Blockchain, let us take 2 traces of blockchain:
π1 & π2.
There are two ways hyperoperties to check here!
1) Non-interference: if some commands are issued by the high-level users (say the general of the army, that should not reach to the ears of the soldier). These should be removable, without the low-level user noticing any changes. 2) Observational Determinism: System should always appear deterministic to the trusted users, or in this case high level users.
Suppose, in the blockchain, there are two traces, π1 & π2.
This is clipped form Dr. Pramod’s teaching. It explains about Observational Determinism, but not with Blockchain
The upper one is π1(set of states as viewed by high level) and lower one is π2(set of states as viewed by low level).
High-Level user is that user, who can make changes to the Blockchain. And Low-level are the ones, who can just look at the states and retrieve data.
Now, whenever some critical input is given by the high level user(like, a general take some decision), it should not be noticed by the low-levels(the soldiers).
So, in OBSERVATIONAL DETERMINISM, the states of blockchain observed by both the low level and high level user should be same. (Notice that obsT between the two traces,showing the observations being made.)
That is all, this has a very crucial implications in the field of Systems, and even larger when applied to Blockchain.
How this could be so big?
This is very big thing. Though introduced back in 2003(observational determinism) & 1982(non interference), these hyperproperties turns out to be very crucial checks in the security.
Just consider a statement:
“If the low level is able to see the change made by the high level, there is the safety issues with Confidentiality adn Intergrity of the data.”
Hope you got a very intuitive feel about these stuff.
Hope you had a great read.
See y’all….