author: aman
Blog III - Part II - Day 12
In this blog, we’ll vaguely discuss the Hyperproperties and Information Flow thing.
As continued, this blog will contain the understandings from the Teachings of Dr Pramod, from SAT SMT Winter School 2018[1]. I will try to portray my understanding from his teachings and is working with him closely on Blockchain, I suppose it earned me a proper understanding.
Let us do this....
In this micro-blog
- Let us check this vaguely
- 2-trace property
- Hyperproperties
- How this could be so big?
Let us check it vaguely
We'll play a game, known as Distinguishability Game.
We pose a challenge game between attacker and a defender, where the attacker needs to exploit flow of information and the defender has to prevent it.
2 people:
attacker | defender |
Situation: There are two systems behind a wall, say system_0 and system_1, and the attacker just have the access to a function foo(x). He doesn't know, whenever he makes a call, to what system does this does the call go to.
The attacker is just like any other user, but who is trying to attack an arrangement behind a wall, popularly known as adversaries.
The defender is the arrangement behind the wall, which diverts the calls to different systems, which have following secret keys: "secret_b" , where b -> {0,1}. i.e. secret_0 or secret_1.
Game Initialisation
- secret_0 := {0,1,2,3}
- secret_1 := {4,5,6,7}
- publicx := {10,11,12,13}
- whenever a normal user makes a call, "only publicx is called, and thus the values inside it are returned"
Game Execution
- there are a lot of calls to foo(x) made from across the world, and by the users with different access levels, i.e. admins & normal user
- so the calls by a normal user are interspersed calls made by the admins
Finalisation
- if attacker is able to identify which system in system_b the call is sent to, he wins, as this information should not be made available to the "normal user"
---> Now consider the following picture
The attacker will try to observe the value of "r", and specially "he will be looking for any unexpected values"
Considering this program, try to make following calls to the system(both normal user and admins included),
• priv_level = sup_user, foo(1), obs = ∅ • priv_level = user, foo(1), obs = 11 • priv_level = sup_user, foo(2), obs= ∅ ........ These calls will go on forever the attacker will
But, now if the program has been like the following, and we bagin with our game:
we start with the following calls, (notice the introduction of variable t)
- priv_level = sup_user, foo(1), obs = ∅
- priv_level = user, foo(4),
- obs = 2 -> b = 0
- obs = 6 -> b = 1
Woosh!!! Did you realise here attacker wins the game, by observing the value of r & t.
If the value returned to the attacker is 2 clearly the secret key b, chosen will be b = 0 and if the value returned to the attacker is 6 clearly the secret key b, chosen will be b = 1
The system just leaked the information.
AFAIK, during my study I encountered this incident had already been reported, where the highly confidential data was leaked due a misprinted "=", I may be wrong though. But, This is a very critical exploitation of Information Flow.
In the very next blog, I'll take a use case of blockchain, and try to determine for such observations for it.
Thanks y'all..
and yeah, Amid this Corona virus thing, be safe...
_ Team CEV