Verifpal 0.19.4

Verifpal 0.19.4 includes bug fixes to analysis logic thanks to reports from "Mike" and Angèle Bossuat (Quarkslab).

Verifpal 0.19.3

Verifpal 0.19.3 includes minor bug fixes to model parsing.

Verifpal 0.19.2

Verifpal 0.19.2 addresses an issue where a primitive returning more outputs than anticipated could result in undefined behavior, as discussed on the Verifpal Mailing List: https://lists.symbolic.software/pipermail/verifpal/2020/000305.html

Verifpal 0.19.1

Verifpal 0.19.1 eliminates some false attacks that could appear with authentication queries and improves sanity checks made on query preconditions.

Verifpal 0.19.0

Verifpal 0.19.0 modifies the behavior of freshness queries.
Now, freshness queries will check if a value is ever *used* while
non-fresh, and not simply contradict the query if a value can ever *be*
non-fresh. This is based on discussions with Eric Simpson.

An example model in examples/test/replay-simple.vp is provided to
illustrate how this is supposed to work.

Verifpal 0.19.0 also fixes a problem that caused VerifHub submissions not
to be possible if Verifpal was installed via Snapcraft, thanks to a patch
submitted by Eric Simpson.

Finally, Verifpal 0.19.0 binaries are built using Go 1.15 (with the exception
of Snapcraft binaries).

Verifpal 0.18.1

Verifpal 0.18.0 removes some misguided "optimizations" to Verifpal's analysis that reduced analysis time but which also led to some missed attacks. As a result, analysis time is now significantly greater.
Verifpal 0.18.1 brings more accurate attack traces.

Verifpal 0.18.0

Verifpal 0.18.0 removes some misguided "optimizations" to Verifpal's analysis that reduced analysis time but which also led to some missed attacks. As a result, analysis time is now significantly greater.

Verifpal 0.17.8

Verifpal 0.17.8 brings minor bug fixes and improvements.

Verifpal 0.17.7

Verifpal 0.17.7 brings minor bug fixes.

Verifpal 0.17.6

Verifpal 0.17.6 brings big improvements to the way Verifpal describes query results. Failed queries now show a lot more information on how the attack was possible.

Verifpal 0.17.5

Verifpal 0.17.5 fixes a bug in Verifpal analysis logic reported by Bruno Blanchet.

Verifpal 0.17.4

Verifpal 0.17.4 fixes a bug in Verifpal analysis logic reported by Bruno Blanchet.

Verifpal 0.17.3

Verifpal 0.17.3 brings performance and speed improvements to Verifpal analysis.

Verifpal 0.17.2

Verifpal 0.17.2 brings performance and speed improvements to Verifpal analysis.

Verifpal 0.17.1

Verifpal 0.17.1 brings performance and speed improvements to Verifpal analysis.

Verifpal 0.17.0

Verifpal 0.17.0 brings improvements to analysis that depends on interleaving sessions.

Verifpal 0.15.6

Verifpal 0.15.6 continues the analysis performance improvements bonanza of the past few days. Consider donating to offset the ridiculous Google Compute Engine bill for the 96-CPU machine that was rented to perform the tests that are leading to this series of improvement updates.

Verifpal 0.15.5

Verifpal 0.15.5 brings further improvements and optimizations to analysis logic.

Verifpal 0.15.4

Verifpal 0.15.4 contains some minor performance improvements.

Verifpal 0.15.3

Verifpal 0.15.3 contains some minor performance improvements.