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@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@google.com> wrote:


On Sat, Oct 17, 2020 at 7:30 AM Nadim Kobeissi <nadim@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:

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:
```
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@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@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@lists.symbolic.software
https://lists.symbolic.software/mailman/listinfo/verifpal


--
See go/tmroeder-availability for my hours and for ways to contact me.


--
See go/tmroeder-availability for my hours and for ways to contact me.