[Verifpal] Defining Behavior When Primitive Returns Less Outputs Than Expected
Nadim Kobeissi
nadim at symbolic.software
Thu Oct 8 20:20:04 CEST 2020
Hello everyone,
It feels like a breath of fresh air to write again to this list! I’m back working on Verifpal after a difficult and busy couple of months, and I’m loving it.
Today I received a bug report from Tom Roeder, in which he demonstrated that the following models, Model A and Model B, caused a crash in Verifpal. Let’s look at Model A:
```
// Model A
attacker[active]
principal Client[
knows private a, b, c, d, e, f
gg = CONCAT(a, b, c)
h = CONCAT(gg, d, e)
]
Client -> Server : h
principal Server[
gc, dc, ec, fc = SPLIT(h)
ac, bc, cc = SPLIT(gc)
]
queries[
authentication? Client -> Server: h
]
```
Here, the cause is obvious: `h` is being split into four values despite being comprised of a concatenation of three values. This should not crash Verifpal, but should reasonably either be defined behavior or throw an error. However, if we look at Model B:
```
// Model B
attacker[active]
principal Client[
knows private a, b, c, d, e, f
gg = CONCAT(a, b, c)
h = CONCAT(gg, d, e, f)
]
Client -> Server : h
principal Server[
gc, dc, ec, fc = SPLIT(h)
ac, bc, cc = SPLIT(gc)
]
queries[
authentication? Client -> Server: h
]
```
Here Verifpal crashes despite the model being sane. This is because the active attacker renders it non-sane by replacing `h` with CONCAT(any, three, values), again triggering the crash when `h` is split into four values despite being a concatenation of three values.
Thus Tom showed that the bug caused a crash in Verifpal in both non-sane (Model A) and sane (Model B) models.
At this point, it became clear that it was important to clearly define Verifpal’s behavior when faced with such instances. I have decided to define it such that any extraneous values are rewritten to `nil`. So, for example, in Model A, on this line:
```
gc, dc, ec, fc = SPLIT(h)
```
`fc` will be rewritten to the `nil` value. This seems to be the most sensible defined behavior for this sort of scenario.
I would be happy to hear your feedback on this decision. The changes are available here and will be part of the next Verifpal update:
https://source.symbolic.software/verifpal/verifpal/-/commit/c5b7702be4fee2439ee8f49851e238e098aafebc
Thanks again to Tom for spotting this issue.
Nadim Kobeissi
Symbolic Software • https://symbolic.software
More information about the Verifpal
mailing list