1. 01 Dec, 2020 1 commit
  2. 29 Nov, 2020 3 commits
  3. 28 Nov, 2020 10 commits
  4. 18 Nov, 2020 1 commit
  5. 14 Nov, 2020 1 commit
  6. 25 Oct, 2020 1 commit
  7. 21 Oct, 2020 5 commits
  8. 20 Oct, 2020 5 commits
  9. 17 Oct, 2020 2 commits
  10. 08 Oct, 2020 5 commits
    • drone's avatar
      Scoop update for verifpal version v0.19.2 · 1d85cde8
      drone authored
      1d85cde8
    • drone's avatar
      Brew formula update for verifpal version v0.19.2 · 162b2a14
      drone authored
      162b2a14
    • Nadim Kobeissi's avatar
      Verifpal 0.19.2 · 998b4d21
      Nadim Kobeissi authored
      998b4d21
    • Nadim Kobeissi's avatar
      Today I received a bug report from Tom Roeder, in which he demonstrated that... · c5b7702b
      Nadim Kobeissi authored
      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.
      c5b7702b
    • Nadim Kobeissi's avatar
      Update go.mod and go.sum · 5e72b0c3
      Nadim Kobeissi authored
      5e72b0c3
  11. 11 Sep, 2020 1 commit
  12. 29 Aug, 2020 1 commit
  13. 27 Aug, 2020 2 commits
  14. 17 Aug, 2020 2 commits