§X uvx OxCaml experiment
Can we use uv to package python? Part of Enki.
§X Read Solving the Bottom Turtle
They’re thinking about a similar problem, but are much more focused on the corporate side.
§X Read Secrets at Scale: Automated Bootstrapping of Secrets & Identity in the Cloud
They just use AWS as their root of trust
§Identity as a Function
Problem
- Service managers have no purview over the lifetimes of the identities networked services create, such as X.509 certificates, DNS records, and protocol-specific keys.
- Such identities are managed in an ad-hoc way that makes it difficult to have insight as to what identities have been created and which might have been compromised.
- There is a complex web of dependencies that makes revoking and rotating identities a manual and error-prone process.
Cost
- Unused identities leave a larger attack surface for access to critical systems, and failure to understand the implications of compromises on downstream identities leaves us vulnerable.
- For example, persisting an outdated SSH key in a server’s
authorized_keyscreates a unnecessary backdoor. - If an attacker gains access to the system, say, running a nameserver, they could move laterally use the ACME protocol to provision TLS certificates for the domain.
- On discovering this compromise all the dependent identities, such as TLS certificates, will need to be revoked.
SOTA
- Existing software deployment techniques layer complexity in order to manage all these identities.
- There’s many useful bits that are stitched together piecemeal with fragile glue, but a lack of a unified interface to identity in the network across disparate protocols.
Solution
- We define a identity Domain Specific Language to describe the types of identities in play in the TCP/IP networking stack, showing the roots of trust in our systems and their transitive dependants.
- By defining identities in this way, we can express identities as functions that return an authentication token, and unclock the programability of identities in the network.
- We can understand the lifetime of identities and garbage collect them when they’re no longer used.
- We can create hundred of honey-pot keys that if used we know there’s been a compromise in the network.
- We can spin up a self-hosted digital island for the duration of a project and manage the full lifetime of the identities involved; from creation, to rotation, to expiry and revocation.
- We can minimising the chain of trust by re-anchoring identities like Matrix user IDs from HTTPS well-known paths to DNSSEC-verified resource-records, using DNSSEC as the narrow waist of trust.
- We can authenticate SSH keys with an AtProto Personal Data Service.
- We provide a framework to understand the roots of trusts of our identities and any weak points in the chain of trust.
Impl
- What if we had registry of identities?
- What are the constituent parts?
- How do we use this language?
- What are we trying to prove?
- Provide clarify to provide to an existing set of rules?
- Are we trying to prove some properties of this system (identities in the network)?
- What is our stunt?
- The service manager could talk to identity service and mount the secrets in a namespace?
- Do we wrap Docker compose?
- Do we implement a service/registry with a Cap’N Proto API that applications can talk to? Using Cap’N Proto as the system call layer.
- Or maybe we can change the mechanism by which the file gets there?
- This is exactly what I’ve done here.
- This is a horrible hack though: the service needs to kill itself to communicate that the downstream dependencies need to restart.
- We’re in this liminal space between building (Nix) and running (SystemD).
§Service Managers a la Carte
They’re just build systems that continue to run. The difference between docker run and docker build is that docker run commands don’t terminate. They’re both sandboxed. Service managers mange to manage dynamic processes: if a service restarts maybe it’s downstream dependencies need to restart.
Starting building block: formalised framework for service managers. It’s within this that we can define what identity is.
What do these systems allow you to express? Restart policies? Are they static or dynamic? None of them are triggered by the fileystem restarting.
It would be insightful to know what the hell goes on on Windows.
A service is a process execution environment and set of dependencies. We have a forest: disjunc graphs with no cycles. Service can be long running or not (just mutate something on the disk/network).
It becomes a build system when the dependencies are run to set up the state of some service. How can we depend on a resource, like a TLS certificate? We could have the service that provides it, and a service that consumes it.
Dune rules service manager.
It is a reactive system (see froc) – you need a notion of time.
§O update the package management paper for arxiv publication
X update formalism
It turns out depopts aren’t a part of the resolution at all, they’re only used to assemble the action graph and order installations from the resolved set of packages. Purely a post-resolution processing step. No depopt we add to any package will actually change the resolved package set; they only change the order in which they’re installed, or whether a package needs to be rebuild given a dependency change.
Some other improvements:
- we don’t add conflicts to the core calculus since we can encode them with a conflict package
- we don’t jump through hoops to support multi-version solving as we encode different cargo package major versions as different package names, with a proxy package to depend on cross-major version bumps
- this means we can resolve for a resolved set of packages and reconstruct their installation order from their dependencies
O Pak language
A maximally expressive lingua franca for package management
O algorithm discussion
We already discuss SAT solving but we should describe Answer-set programming solutions like PubGrub, and how CUDF fits in here
O bidirectional translations - [[*$$\[https://github.com/RyanGibb/uvx-ocaml$$uvxOxCaml\] experiment][opam to uv]]
O what can we reason about with the package calculus?
- diamond dependency problem?
- how to extract it from an arbitrarily complex graph?