[Verifpal] Defining Behavior When Primitive Returns Less Outputs Than Expected

Nadim Kobeissi nadim at symbolic.software
Thu Oct 15 21:20:02 CEST 2020


Dear Tom,

Just to let you know that I do plan to look at this this week.

Nadim Kobeissi
Symbolic Software • https://symbolic.software

> On 12 Oct 2020, at 9:37 PM, Tom Roeder <tmroeder at google.com> wrote:
> 
> Thanks, Nadim, for the quick fix.
> 
> I can confirm that this solves that crash in analyzing my model.
> 
> However, my full model still causes Verifpal to crash. I've been trying to minimize the test case, and I can't eliminate much of the model without also eliminating the crash. I plan to release this model publicly, but I haven't yet asked the internal open-source office here at Google for permission to do that. So, I don't think I can send you the full model file to debug on your side.
> 
> I'm going to keep trying to minimize the model and debug the crash, but I'm not sure how much more time I can put into it. If you have any suggestions that would help narrow down the model line it came from, that might help me produce a minimized test case.
> 
> The traceback I get is from nearly exactly the same place in the code.
> 
> panic: runtime error: index out of range [2] with length 2
> 
> goroutine 1243 [running]:
> verifpal.com/cmd/vplogic.valuePerformPrimitiveRewrite(0xc00022b1b5, 0x5, 0xc002272140, 0x1, 0x1, 0x2, 0x0, 0xffffffffffffffff, 0xc000021580, 0x3, ...)
>         verifpal.com/cmd/vplogic/value.go:246 +0xb50
> verifpal.com/cmd/vplogic.valuePerformEquationRewrite(0xc000507040, 0x2, 0x2, 0x48, 0xc000021580, 0x3, 0xc000d22a00, 0x59, 0x59, 0xc002418000, ...)
>         verifpal.com/cmd/vplogic/value.go:321 +0xbaa
> verifpal.com/cmd/vplogic.valuePerformAllRewrites(0xc000021580, 0x3, 0xc000d22a00, 0x59, 0x59, 0xc002418000, 0x59, 0x59, 0xc000b60900, 0x59, ...)
>         verifpal.com/cmd/vplogic/value.go:378 +0x157
> verifpal.com/cmd/vplogic.verifyActiveMutatePrincipalState(0xc000021580, 0x3, 0xc000d22a00, 0x59, 0x59, 0xc002418000, 0x59, 0x59, 0xc000b60900, 0x59, ...)
>         verifpal.com/cmd/vplogic/verifyactive.go:164 +0x4f3
> verifpal.com/cmd/vplogic.verifyActiveScan(0xc0002e5200, 0x3, 0x4, 0xc000332000, 0x59, 0x92, 0xc000320000, 0x59, 0x8f, 0xc0001a3800, ...)
>         verifpal.com/cmd/vplogic/verifyactive.go:86 +0x229
> verifpal.com/cmd/vplogic.verifyActiveScan.func2(0xc002f7e0c0, 0xc00231c780, 0x1, 0x0, 0xc000205500, 0x52, 0x8f, 0xc000e1e000, 0x52, 0x80, ...)
>         verifpal.com/cmd/vplogic/verifyactive.go:109 +0x1a1
> created by verifpal.com/cmd/vplogic.verifyActiveScan
>         verifpal.com/cmd/vplogic/verifyactive.go:108 +0x3b2
> 
> 
> Can you add some unit tests or use the "testing/quick" package (QuickCheck for Go) to test this part of the code?
> 
> On Thu, Oct 8, 2020 at 11:20 AM Nadim Kobeissi via Verifpal <verifpal at lists.symbolic.software> wrote:
> 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
> 
> 
> _______________________________________________
> Verifpal mailing list
> Verifpal at lists.symbolic.software
> https://lists.symbolic.software/mailman/listinfo/verifpal



More information about the Verifpal mailing list