[Verifpal] Verifpal 0.4.1 crash

[Nadim Kobeissi]

Dear Renaud,

The crash is fixed in the latest master code, and the Signal verification
time increase is unfortunately not a bug.

Thank you very much for your input, and hoping to hear from you again.

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


On Thu, Sep 5, 2019 at 7:27 AM Renaud Lifchitz via Verifpal
<verifpal at lists.symbolic.software> wrote:

> Hello,
>
> Using Verifpal 0.4.1 with included example protonmail_to_outside.vp leads
> to a crash:
> (...)
> Deduction! AEAD_ENC(ga^b, m2, ga) found by attacker by equivocating with
> em2 (analysis 104, depth 1)
> panic: runtime error: index out of range
>
> goroutine 1 [running]:
> main.sanityResolveInternalValues(0x5052de, 0x8, 0x0, 0x0, 0x0, 0x0, 0x0,
> 0x0, 0x0, 0x0, ...)
> /home/renaud/installations/verifpal/internal/app/verifpal/sanity.go:487
> +0x1037
> main.verifyAnalysisReconstruct(0x5052de, 0x8, 0x0, 0x0, 0x0, 0x0, 0x0,
> 0x0, 0x0, 0x0, ...)
> /home/renaud/installations/verifpal/internal/app/verifpal/verifyanalysis.go:125
> +0x65
> main.verifyAnalysis(0xc0000aa040, 0xc0000cd900, 0xc0004a2050, 0x95, 0x0,
> 0x1)
> /home/renaud/installations/verifpal/internal/app/verifpal/verifyanalysis.go:27
> +0x21d
> main.verifyActive(0xc0000aa040, 0xc0000cbd80, 0x0, 0x0, 0x505326)
> /home/renaud/installations/verifpal/internal/app/verifpal/verifyactive.go:26
> +0x54f
> main.verify(0xc0000aa040, 0xc0000cbd80, 0xc0000aa040, 0xc0000cbd80, 0x1)
> /home/renaud/installations/verifpal/internal/app/verifpal/verify.go:23
> +0x4e1
> main.main()
> /home/renaud/installations/verifpal/internal/app/verifpal/main.go:40 +0x2ef
>
> and verifying included signal.vp seems to take a very long time to
> complete due to recent changes in the code...
>
> Thank you.
>
> Best regards,
>
> Renaud Lifchitz
>
>
> _______________________________________________
> Verifpal mailing list
> Verifpal at lists.symbolic.software
> https://lists.symbolic.software/mailman/listinfo/verifpal
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20190905/7a8a4dce/attachment.htm>