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

Tom Roeder tmroeder at google.com
Wed Oct 21 01:30:43 CEST 2020


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/20201020/0dca9434/attachment-0001.htm>


More information about the Verifpal mailing list