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

Nadim Kobeissi nadim at symbolic.software
Tue Oct 20 23:22:04 CEST 2020


 Dear Tom,

> Sorry, this still doesn't solve the problem, though I do get a different
crash:
> panic: runtime error: index out of range [-1]

Could you please pull down from master, build and try again, I just pushed
this commit:
https://source.symbolic.software/verifpal/verifpal/-/commit/5cf300416d975e36e6d30ace932ad0924ce88b03

I wish I could see the model causing this issue, but alas.

> I don't follow the claim that a functional programming style avoids the
need for unit tests.

To be clear, I never said or implied this. :-)

> Integration tests are necessary but are not sufficient because they are
difficult to tune to get sufficient code coverage.

You've certainly made your point.

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


Thank you, I will take a look at both this and QuickCheck.

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


On Tue, Oct 20, 2020 at 11:00 PM Tom Roeder <tmroeder at google.com> wrote:

>
>
> 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/04d11bf0/attachment-0001.htm>


More information about the Verifpal mailing list