hum-lang/examples/session_server.hum at main · undergroundrap/hum-lang · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
app session_server {
  why:
    accept trusted users and keep their sessions fast, safe, and memory efficient

  uses:
    network
    clock
    random.secure

  starts with:
    start_server

  task start_server -> Unit {
    why:
      mark the structural executable root without claiming server IO exists

    does:
      return
  }

  store sessions: map SessionId -> Session {
    expects:
      up to 20 million active sessions

    optimizes:
      lookup speed
      memory density
      collision resistance

    protects:
      session ids cannot be guessed
      expired sessions cannot be reused

    hides:
      hash layout
      bucket metadata
      resize strategy
  }

  type Session {
    user: UserId
    created_at: Time
    expires_at: Time

    keeps:
      expires_at is after created_at
  }

  task create_session(user: User, device: Device) -> SessionToken {
    why:
      let a verified user stay signed in without sending their password again

    uses:
      user.id
      device.fingerprint
      clock.now
      random.secure
      sessions

    changes:
      sessions

    needs:
      user is verified
      device is allowed

    ensures:
      token belongs to user
      token expires in 30 days
      token does not reveal user secrets

    protects:
      session id cannot be guessed
      expired token cannot work

    trusts:
      random.secure is cryptographically strong
      clock.now does not move backward by more than 5 minutes

    watch for:
      attacker may create many sessions quickly
      hash collisions must not make lookup slow
      memory use must stay bounded
      clock skew must not create immortal sessions

    cost:
      time: O(1)
      space: O(1)
      check: warn

    allocates:
      one session record
      no unbounded temporary buffers

    optimizes:
      lookup speed
      memory density
      secure randomness over raw speed

    tests:
      many users creating sessions at once
      expired token is rejected
      repeated random collision attempts stay bounded

    does:
      make secure token
      create session for user
      save session by token id in sessions
      return token
  }
}