Session TTL inequalities

[vitorenesduarte]

1. Why we may not want to support ">"

• If e.g. ttl > 1h, the user would probably want us to select 1h (+1s) as the ttl (but 2h would also be valid given the inequality).
• If e.g. ttl < 1h, the user would probably want us to select 1h (-1s) as the ttl (but 1min would also be valid given the inequality).

In the first case we're selecting the least permissive value, while in the second case we're selecting the most permissive value, and so it seems that there's no consistent rule that could be applied.

2. Why we may not want to support "=="

Consider the following two predicates A and B, and their logical and & or:

A	B	A and B	A or B
ttl == 1h	ttl == 2h	False	ttl == 1h or ttl == 2h
ttl < 1h	ttl == 2h	False	ttl == 1h or ttl < 2h
ttl == 1h	ttl < 2h	ttl == 1h	ttl < 2h
ttl < 1h	ttl < 2h	ttl < 1h	ttl < 2h

As we can see, the use of == allows the user to specify predicates that are logically false, and so we probably should not support it.

We're left only with "<"

Given points 1. and 2. above, we're left only with "<".

As we can see in the above table, we have only two possibilities when using only "<":

• ttl < 1h and ttl < 2h (which evaluates to ttl < 1h)
• ttl < 1h or ttl < 2h (which evaluates to ttl < 2h)

Computing point values from inequalities using Z3

Assuming the above, any TTL inequality will evaluate to something of the following form ttl < N. In this case, we could argue that the policy should be exported with max_session_ttl: N.

If we simply ask Z3 to solve ttl < N, it will output a model with the smallest value satisfying the inequality (i.e. ttl: 0).

However, we can simply negate ttl < N (i.e. ttl >= N), and Z3 will output exactly what we want (i.e. ttl: N).

The code example below shows this:

from z3 import *

ttl = Int('ttl')

exprs = [
    And(ttl < 1, ttl < 2), # ttl < 1
    Or(ttl < 1, ttl < 2)   # ttl < 2
]
for expr in exprs:
    for expr in [expr, Not(expr)]:
        print("expr:  {}".format(expr))
        s = Solver()
        s.add(expr)
        _ = s.check()
        print("model: {}".format(s.model()))
        print()

expr:  And(ttl < 1, ttl < 2)
model: [ttl = 0]

expr:  Not(And(ttl < 1, ttl < 2))
model: [ttl = 1]

expr:  Or(ttl < 1, ttl < 2)
model: [ttl = 0]

expr:  Not(Or(ttl < 1, ttl < 2))
model: [ttl = 2]

[klizhentas]

@vitorenesduarte the reason I like inequalities for export and for spec is because they make it very explicit what's happening behind the scenes today with TTL.

max_session_ttl: N does not really comminicates to the reader that the min value will be chosen or have been chosen out of two, while max_session_ttl < N does. So I would like us to keep the inequality format because it reflects closer what exactly predicate does (constraints and theorem) to avoid implicit behind-the-scenes conversions as much as possible (although not always possible)

[vitorenesduarte]

@vitorenesduarte the reason I like inequalities for export and for spec is because they make it very explicit what's happening behind the scenes today with TTL.

max_session_ttl: N does not really comminicates to the reader that the min value will be chosen or have been chosen out of two, while max_session_ttl < N does. So I would like us to keep the inequality format because it reflects closer what exactly predicate does (constraints and theorem) to avoid implicit behind-the-scenes conversions as much as possible (although not always possible)

I was thinking that we wanted to have point values (max_session_ttl: N) in the exported policies. Nonetheless, the solver idea proposed in issue description can also be used to output max_session_ttl < N.