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

Tom Roeder tmroeder at google.com
Tue Oct 20 22:59:42 CEST 2020


On Sat, Oct 17, 2020 at 7:30 AM Nadim Kobeissi <nadim at symbolic.software>
wrote:

> 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
>

Sorry, this still doesn't solve the problem, though I do get a different
crash:

panic: runtime error: index out of range [-1]

goroutine 1220 [running]:
verifpal.com/cmd/vplogic.valuePerformPrimitiveRewrite(0xc000204c75, 0x5,
0xc0016bd9a0, 0x1, 0x1, 0x2, 0x0, 0xffffffffffffffff, 0xc000123040, 0x3,
...)
        verifpal.com/cmd/vplogic/value.go:233 +0xbad
verifpal.com/cmd/vplogic.valuePerformEquationRewrite(0xc0029a3900, 0x2,
0x2, 0x48, 0xc000123040, 0x3, 0xc002350a00, 0x59, 0x59, 0xc001700000, ...)
        verifpal.com/cmd/vplogic/value.go:321 +0xbaa
verifpal.com/cmd/vplogic.valuePerformAllRewrites(0xc000123040, 0x3,
0xc002350a00, 0x59, 0x59, 0xc001700000, 0x59, 0x59, 0xc0016b0180, 0x59, ...)
        verifpal.com/cmd/vplogic/value.go:378 +0x157
verifpal.com/cmd/vplogic.verifyActiveMutatePrincipalState(0xc000123040,
0x3, 0xc002350a00, 0x59, 0x59, 0xc001700000, 0x59, 0x59, 0xc0016b0180,
0x59, ...)
        verifpal.com/cmd/vplogic/verifyactive.go:164 +0x4f3
verifpal.com/cmd/vplogic.verifyActiveScan(0xc0002a7080, 0x3, 0x4,
0xc000302000, 0x59, 0x92, 0xc0002f0000, 0x59, 0x8f, 0xc00015f800, ...)
        verifpal.com/cmd/vplogic/verifyactive.go:86 +0x229
verifpal.com/cmd/vplogic.verifyActiveScan.func2(0xc0006ee0c0, 0xc001e88180,
0x1, 0x0, 0xc000285500, 0x52, 0x8f, 0xc000fe0000, 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

I'm planning to start the process of getting this model released under an
open-source license, and I'll try to get it out soon. I understand that
it's difficult to debug this issue blindly, from only the backtrace. So,
I'll wait to work on this again until I can release the model.


>
> 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 don't follow the claim that a functional programming style avoids the
need for unit tests. For example, QuickCheck actually originally comes from
Haskell (a pure functional language) and the Haskell community also uses
HUnit and other unit testing frameworks extensively. Integration tests are
necessary but are not sufficient because they are difficult to tune to get
sufficient code coverage.

I would still strongly recommend adding unit tests as a way to improve the
robustness of Verifpal. The Go language makes it very easy, including
providing built-in tools for checking the coverage of your tests:  see
https://blog.golang.org/cover.


>
> 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
>>
>>

-- 
See go/tmroeder-availability for my hours and for ways to contact me.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20201020/9a07636e/attachment-0001.htm>


More information about the Verifpal mailing list