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

Nadim Kobeissi nadim at symbolic.software
Wed Oct 21 10:38:15 CEST 2020


> Verifpal currently shows "Stage 1, Analysis 1200000" and is working on
it.

That's not a good sign. Stage 1 is supposed to finish up very quickly, and
if you're at that many analysis mutations on stage 1 alone it's likely your
analysis will take a *very* long time.

I hope you'll get to share your model soon because I might be able to offer
suggestions on shortening the analysis time without making the protocol
model less expressive. You might also want to get a strong workstation.

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


On Wed, Oct 21, 2020 at 1:31 AM Tom Roeder <tmroeder at google.com> wrote:

> Thanks! I'm happy to report that the most recent change did solve the
> crashes I was seeing. Verifpal currently shows "Stage 1, Analysis 1200000"
> and is working on it.
>
> I'll let you know when I can share the model publicly.
>
> On Tue, Oct 20, 2020 at 2:22 PM Nadim Kobeissi <nadim at symbolic.software>
> wrote:
>
>> 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. :-)
>>
>
> Sorry, it looks like I was reading too much into the text.
>
>
>>
>> > 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
>>> <https://goto.google.com/tmroeder-availability> for my hours and for
>>> ways to contact me.
>>>
>>
>
> --
> 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/20201021/eddba51c/attachment-0001.htm>


More information about the Verifpal mailing list