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

Nadim Kobeissi nadim at symbolic.software
Sat Oct 17 16:30:19 CEST 2020


Dear Tom,

Thank you for your continued feedback on this important issue.

I am having trouble fully understanding the issue you are facing given the
constraints imposed by your employer on how much of your Verifpal model you
can share. However, based on some reasonably fair assumptions, I have
submitted the following commit which I believe might fix the issue once and
for all:
https://source.symbolic.software/verifpal/verifpal/-/commit/32a2ab40050679d7455c6aa99558fcfa58444542

In order for you to test this fix, you will need to do the following:
```
git clone https://source.symbolic.software/verifpal/verifpal.git
cd verifpal
make
./build/macos/verifpal verify path/to/myConfidentialModel.vp
```

In the above, you will need to replace `./build/macos/verifpal` with
`./build/linux/verifpal`or  `./build/windows/verifpal.exe` depending on
your preferred operating system.

>  Can you add some unit tests or use the "testing/quick" package
(QuickCheck for Go) to test this part of the code?

Verifpal follows a purely functional programming style which encourages
clear definitions for each component of the analysis logic and operations
on the model state with no side effects. For testing, Verifpal relies not
on unit tests but on an integration test approach, which runs Verifpal
against expected results on 54 models, located in `examples/test`. I have
tested this proposed fix using the integration tests as well as on "Model
A" and "Model B" from our previous discussion.

I am keen to know if this fix addresses the issue for you, so please keep
in touch.

Nadim Kobeissi
Symbolic Software • https://symbolic.software
Sent from office


On Mon, Oct 12, 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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20201017/637dc3b6/attachment.htm>


More information about the Verifpal mailing list