Joana Fig. 3 top right
Example from 'A new algorithm for low-deterministic security', D. Giffhorn and G. Snelting, International Journal of Information Security, 2015. Figure 3, top right.
// Example from "A new algorithm for low-deterministic security"
// D. Giffhorn and G. Snelting
// International Journal of Information Security, 2015
// Figure 3, top right
method inputPIN() returns (res: Int)
method print(val: Int)
requires low(val)
requires lowEvent
method main()
requires lowEvent
{
var x: Int
x := inputPIN()
var willterm : Bool := x >= 0
// Loop has termination leak
while (x != 0) // verification fails because termination condition is high
terminates x >= 0 with x >= 0 ? x : 0
invariant willterm ==> x >= 0
invariant !willterm ==> x < 0
{
x := x - 1
}
print(1)
}
// fixed version with declassification
method main_fixed()
requires lowEvent
{
var x: Int
x := inputPIN()
declassify x >= 0
var willterm : Bool := x >= 0
while (x != 0)
terminates x >= 0 with x >= 0 ? x : 0
invariant willterm ==> x >= 0
invariant !willterm ==> x < 0
{
x := x - 1
}
print(1)
}