Analysing Web-app Authentication Logic

When writing and refactoring we often have to make a lot of assumptions about how our code works. Here we'll look at some example authentication logic written in OCaml that you might find a standard web application codebase, and use Imandra as a tool to analyse it.

Let's imagine our system currently has a user represented by this type:

In [1]:
type user =
{ is_admin: bool
; username: string
; email: string
}
Out[1]:
type user = { is_admin : bool; username : string; email : string; }

Right. Let's take a look at the core of the authentication logic itself.

In [2]:
type auth_result = Authed | Not_authed;;

let get_auth_result (path: string) (u : user) : auth_result =
    if String.prefix "/user/" path then
        if String.prefix ("/user/" ^ u.username) path then
            Authed
        else
            Not_authed
    else if String.prefix "/admin" path then
        if u.is_admin then
            Authed
        else
            (* Temporary hack to give co-founder accounts admin access for the demo! - DA 06/05/15 *)
            if List.exists (fun au -> au = u.username) ["diego"; "shannon"] then
                Authed
            else
                Not_authed
    else
        Authed
Out[2]:
type auth_result = Authed | Not_authed
val get_auth_result : string -> user -> auth_result = <fun>

There's even a few tests (although they are a bit rusty...)!

In [3]:
type test_result = Pass | Fail;;
let run_test f = if f then Pass else Fail;;
Out[3]:
type test_result = Pass | Fail
val run_test : bool -> test_result = <fun>
In [4]:
run_test ((get_auth_result "/" { username = "test"; email = "email"; is_admin = false }) = Authed);;
run_test ((get_auth_result "/admin" { username = "test"; email = "email"; is_admin = false }) = Not_authed);;
run_test ((get_auth_result "/admin" { username = "test"; email = "email"; is_admin = true }) = Authed);;
run_test ((get_auth_result "/user/paula" { username = "joe"; email = "email"; is_admin = false } = Not_authed));;
run_test ((get_auth_result "/user/paula" { username = "paula"; email = "email"; is_admin = false } = Authed));;
run_test ((get_auth_result "/user/paula/profile" { username = "paula"; email = "email"; is_admin = false } = Authed));;
Out[4]:
- : test_result = Pass
- : test_result = Pass
- : test_result = Pass
- : test_result = Pass
- : test_result = Pass
- : test_result = Pass

However the tests haven't quite covered all the cases. Let's use Imandra to verify a few things. Note that we've got tests for is_admin = true (test 2) and is_admin = false (test 3) on the /admin route above, but this only checks that these inputs give the desired outcome, and not that all inputs do. So let's verify that all non-admin users are not authenticated for the admin area.

In [5]:
verify (fun u -> u.is_admin = false ==> (get_auth_result "/admin" u) = Not_authed)
Out[5]:
- : user -> bool = <fun>
module CX : sig val u : user end
Counterexample (after 1 steps, 0.010s):
 let (u : user) = {is_admin = false; username = "diego"; email = "diego"}
Refuted
proof attempt
ground_instances1
definitions0
inductions0
search_time
0.010s
details
Expand
smt_stats
num checks3
rlimit count718
mk clause10
datatype occurs check24
seq add axiom2
mk bool var24
decisions4
seq num reductions10
propagations4
interface eqs2
conflicts1
datatype accessor ax6
datatype constructor ax1
seq extensionality2
num allocs1012159006
final checks4
added eqs20
del clause6
memory22.330000
max memory26.950000
Expand
  • start[0.010s]
      :var_0:.is_admin = false
      ==> (if String.prefix "/user/" "/admin"
           then
             if String.prefix (String.append "/user/" :var_0:.username) "/admin"
             then Authed else Not_authed
           else
           if String.prefix "/admin" "/admin"
           then
             if :var_0:.is_admin then Authed
             else
             if List.exists ((fun u au -> au = u.username) :var_0:) …
             then Authed else Not_authed
           else Authed)
          = Not_authed
  • simplify

    into
    :var_0:.is_admin
    || (if :var_0:.is_admin then Authed
        else
        if List.exists ((fun u au -> au = u.username) :var_0:)
           ("diego" :: (… :: …))
        then Authed else Not_authed)
       = Not_authed
    expansions
    []
    rewrite_steps
      forward_chaining
      • unroll
        expr
        (|`List.exists (anon_fun.get_auth_result.0 (u : user))[0]`_1898|
          u_31
          (|::_3| "diego" (|::_3| "s…
        expansions
        • Sat (Some let (u : user) = {is_admin = false; username = "diego"; email = "diego"} )

        This verification fails, and Imandra gives us an example input that violates the assumption we gave it - we hadn't considered the users added by the 'temporary hack' code path in our tests!

        We can also ask for a decomposition of all the regions in the get_auth_result function, which gives us an idea of the various conditions and complexity:

        In [6]:
        let d = Modular_decomp.top "get_auth_result" [@@program];;
        Modular_decomp.prune d;; 
        d
        
        Out[6]:
        val d : Top_result.modular_decomposition =
          {Imandra_interactive.Modular_decomp.MD.md_session = 1i;
           md_f =
            {Imandra_surface.Uid.name = "get_auth_result"; id = <abstr>;
             special_tag = <abstr>; namespace = <abstr>;
             chash = Some rvO02H9cq1SzD0d2m7FQQvFO1H743y6ERAMEhrXoJFk;
             depth = (4i, 2i)};
           md_args = [(path : string); (u : user)]; md_regions = <abstr>}
        - : unit = ()
        - : Top_result.modular_decomposition =
        {Imandra_interactive.Modular_decomp.MD.md_session = 1i;
         md_f =
          {Imandra_surface.Uid.name = "get_auth_result"; id = <abstr>;
           special_tag = <abstr>; namespace = <abstr>;
           chash = Some rvO02H9cq1SzD0d2m7FQQvFO1H743y6ERAMEhrXoJFk;
           depth = (4i, 2i)};
         md_args = [(path : string); (u : user)]; md_regions = <abstr>}
        
        Regions details

        No group selected.

        • Concrete regions are numbered
        • Unnumbered regions are groups whose children share a particular constraint
        • Click on a region to view its details
        • Double click on a region to zoom in on it
        • Shift+double click to zoom out
        • Hit escape to reset back to the top
        decomp of (get_auth_result path, u
        Reg_idConstraintsInvariant
        5
        • not (String.prefix "/admin" path)
        • not (String.prefix "/user/" path)
        Authed
        4
        • not (List.exists ((fun u au -> au = u.username) u) ["diego"; "shannon"])
        • not u.is_admin
        • String.prefix "/admin" path
        • not (String.prefix "/user/" path)
        Not_authed
        3
        • List.exists ((fun u au -> au = u.username) u) ["diego"; "shannon"]
        • not u.is_admin
        • String.prefix "/admin" path
        • not (String.prefix "/user/" path)
        Authed
        2
        • u.is_admin
        • String.prefix "/admin" path
        • not (String.prefix "/user/" path)
        Authed
        1
        • not (String.prefix (String.append "/user/" u.username) path)
        • String.prefix "/user/" path
        Not_authed
        0
        • String.prefix (String.append "/user/" u.username) path
        • String.prefix "/user/" path
        Authed