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