Combine options outside of Z3

[vitorenesduarte]

This PR is the first step towards #43.

It only focus on the following options for now:

• max_session_ttl
• recording_mode
• source_ip

The idea is to gather feedback on the general approach implemented here before implementing the remaining options.

From option inequalities to a simple struct

Before this PR, options were specified using inequalities. Instead now we have:

    p = Policy(
        name="access",
        options=Options(
            max_session_ttl=Duration.new(hours=10),
            recording_mode=RecordingMode.STRICT,
            source_ip=SourceIp.PINNED,
        ),
        allow=Rules(
            AccessNode(
                (User.traits["team"] == ("admins",))
            ),
        ),
    )

With predictable option combining (#43) there's no need to say max_session_ttl < 10h to try to imply that the min will be chosen in case two of these are combined.

Combining two of these inequalities using logical AND also doesn't seem to make sense.
If we say max_session_ttl < 10 AND max_session_ttl < 3, this is equivalent to max_session_ttl < 3
When Z3 solves this (see the solver proposed in #27) it will output max_session_ttl == 0 as that's a valid solution.

In general, saying max_session_ttl < 3 could be interpreted as "max_session_ttl can have any value smaller than 3", but this is not exactly what we want it to mean.

Option combining

Option combining is implemented outside of Z3 as it's very easy to do so (e.g. just call min).

export output

As options are not defined using inequalities, the export command now outputs them as a list.

predicate export examples/access.py outputs the following:

kind: policy
metadata:
  name: access
spec:
  allow:
    access_node: (((access_node.login == user.name) && (!(user.name == "root"))) ||
      equals(user.traits["team"], ["admins"]))
  deny:
    access_node: (((access_node.login == "mike") || (access_node.login == "jester"))
      || (node.labels["env"] == "prod"))
  options:
    max_session_ttl: 36000000000000
    recording_mode: strict
    source_ip: pinned
version: v1

Other changes

While working on this I made some general improvements:

• ran linter (fixed issues and formatted the code)
• added linter to CI (hit ignore-missing-import option does not work on false positive "Library stubs not installed for X" python/mypy#10632, which took many iterations to solve)
• simplified the README so that it points to the examples folder and doesn't contain outdated information
• ran poetry update which updated poetry.lock
• removed some unused functions
• added types to some functions
• added a TeleportSolverResult that encapsulates the outcomes of the solver
• removed LtDuration as it's no longer needed
• simplified build_predicate

[klizhentas]

@vitorenesduarte

• please use the Z3 solver instead of custom solver here. Using Z3 solver makes it impossible to create proper query. You can build your own solver using max strategy so 0 won't be a solution. You have to find a maximum value that satisfies both equations.

• please use inequalities as they demonstrate the intent much better and you can query - with more granularity, for example, you can say, is it possible to get a certificate less than 10 minutes? With inequalities and Z3 solver the answer will be correct, with your proposed solution it is not possible.

• Write a test example with the case above to demonstrate the benefit.

[xacrimon]

Close for now