Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
39 changes: 39 additions & 0 deletions dag/extdeps/container/docker_engine.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,39 @@
module extdeps.container.docker_engine

import extdeps.container.engine { ContainerEngine, RootfulDaemon, RootlessDaemon }
import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef }
import extdeps.uri { Uri, Https }
import extdeps.vendor.docker_inc { docker_inc }
import std.decl_ref { DeclarationRef, WholeDeclaration }

data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
uri: Uri {
scheme: Https
locator: "docs.docker.com/engine/security/rootless/"
}
}

data extdeps_model_scope: ExternalModelScope = ExternalModelScope {
subject: ExternalSubjectRef {
declaration: DeclarationRef {
module_path: "extdeps.container.docker_engine",
decl_name: "docker_engine",
field: WholeDeclaration
}
},
first_citation: extdeps.container.docker_engine.extdeps_external_authority_anchor,
further_citations: []
}

// Docker Engine as a PRODUCT. Its Ubuntu apt distribution is a separate fact and keeps its own
// module (extdeps.container.docker_ce): how you install it is not what it is.
//
// Both privilege modes are cited: the rootless mode is documented at the anchor above as a
// supported way to run the daemon and the CLI as a non-root user, and the default installation is
// the rootful daemon that same page contrasts it with. The fleet runs the rootless mode, and that
// is recorded where the fleet is described, not here.
data docker_engine: ContainerEngine = ContainerEngine {
vendor: docker_inc,
product_name: "Docker Engine",
privilege_modes: [RootfulDaemon, RootlessDaemon],
}
102 changes: 102 additions & 0 deletions dag/extdeps/container/engine.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,102 @@
module extdeps.container.engine

import extdeps.external_authority { ExternalAuthority }
import extdeps.software { Software }
import extdeps.uri { Uri, Https }
import extdeps.vendor { Vendor }
import std.types { Bool, List, NonEmptyStr, String }

data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
uri: Uri {
scheme: Https
locator: "github.com/opencontainers/runtime-spec/blob/main/spec.md"
}
}

// THE AGNOSTIC SHAPE OF A THING THAT RUNS AN OCI IMAGE, WITH NO PRODUCT ENUMERATED IN IT.
//
// This hub defines what a container engine IS. It does not name Docker, Podman or anything else,
// and it deliberately carries no `match` over products: enumerating them here is precisely the case
// DESIGN's external-upstream-decomposition section rules out with "adding Opera must not widen a
// generic browser-product enum". Each engine is an independently versioned upstream product with
// its own module authority and its own cited row; adding one is a new file, never an edit here.
//
// WHAT THIS REPLACES. `gunbc.fleet_intent` carried
// type ContainerRuntime = Docker | Podman | Gvisor | Ubicloud | GcloudRun
// which fused three unrelated concepts into five members of one enum: container engines (Docker,
// Podman), a sandboxing runtime whose whole point is the isolation guarantee it adds (gVisor), and
// two companies that rent you a machine (Ubicloud, Google Cloud Run). Widening it was the only way
// to add either an engine or a supplier, so the two questions could never be asked separately.

type EnginePrivilegeMode
= RootfulDaemon
| RootlessDaemon

fn engine_privilege_mode_label(mode: EnginePrivilegeMode) -> String {
match mode {
RootfulDaemon => "rootful"
RootlessDaemon => "rootless"
}
}

// A PRODUCT CAPABILITY ROW, NOT A DEPLOYMENT.
//
// `privilege_modes` is what the PRODUCT supports, cited to its own docs. Which mode a particular
// host actually runs is a fact about that host and lives on the deployment below -- the
// interface / realization / policy split of DESIGN section 3. Fusing them is how "we run Docker"
// came to mean nothing about whether the daemon is root, which is the one property that decides
// whether a compromised job owns the machine.
type ContainerEngine {
vendor: Vendor<Software>
product_name: NonEmptyStr
privilege_modes: List<EnginePrivilegeMode>
}

fn container_engine_supports_privilege_mode(engine: ContainerEngine, mode: EnginePrivilegeMode) -> Bool {
any(engine.privilege_modes, m => m == mode)
}

type EngineDeploymentRefusal
= PrivilegeModeUnsupported { product_name: NonEmptyStr, mode: EnginePrivilegeMode }

// WHAT IS ACTUALLY INSTALLED SOMEWHERE, WHICH IS THE ENGINE PLUS ONE CHOICE ABOUT IT.
type ContainerEngineDeployment {
engine: ContainerEngine
privilege_mode: EnginePrivilegeMode
}

type ContainerEngineDeploymentOutcome
= ContainerEngineDeployed { deployment: ContainerEngineDeployment }
| ContainerEngineDeploymentRefused { refusal: EngineDeploymentRefusal }

// Claiming a mode the product does not offer is a declaration that cannot be true, so it refuses
// here rather than being carried as a surface fact nothing ever checks.
fn container_engine_deployment(
engine: ContainerEngine,
privilege_mode: EnginePrivilegeMode,
) -> ContainerEngineDeploymentOutcome {
if container_engine_supports_privilege_mode(engine: engine, mode: privilege_mode) {
ContainerEngineDeployed {
deployment: ContainerEngineDeployment { engine: engine, privilege_mode: privilege_mode },
}
} else {
ContainerEngineDeploymentRefused {
refusal: PrivilegeModeUnsupported {
product_name: engine.product_name,
mode: privilege_mode,
},
}
}
}

fn container_engine_deployment_label(deployment: ContainerEngineDeployment) -> String {
join(
[
deployment.engine.product_name as String,
" (",
engine_privilege_mode_label(mode: deployment.privilege_mode),
")",
],
"",
)
}
60 changes: 45 additions & 15 deletions dag/extdeps/container/oci/image_config.dag
Original file line number Diff line number Diff line change
Expand Up @@ -57,28 +57,57 @@ fn image_config_layer_count(c: ImageConfiguration) -> Int {
}
}

// THE BARE-BINDING ARM DID NOT UNWRAP, AND NOTHING NOTICED BECAUSE NOTHING RAN.
//
// This read `match c.config { null => [] ; cfg => match cfg.Entrypoint { ... } }`. The bare arm
// binds the OPTIONAL, not its payload, so the inner field read refused at runtime with
// `NoSuchField { type_name: "Optional", field: "Entrypoint" }`. It typechecked and had witnesses,
// and the defect surfaced the first time a consumer actually called it -- which is precisely the
// specification-without-execution failure DESIGN section 5 names, found the way that section says
// it is found. Present/Absent binds the payload.
fn image_config_entrypoint(c: ImageConfiguration) -> List<String> {
match c.config {
null => []
cfg =>
Absent => []
Present { value: cfg } =>
match cfg.Entrypoint {
null => []
ep => ep
Absent => []
Present { value: entrypoint } => entrypoint
}
}
}

fn image_config_cmd(c: ImageConfiguration) -> List<String> {
match c.config {
Absent => []
Present { value: cfg } =>
match cfg.Cmd {
Absent => []
Present { value: cmd } => cmd
}
}
}

// THE COMMAND A RUNTIME WOULD ACTUALLY EXECUTE, WHICH NEITHER FIELD ANSWERS ALONE.
//
// config.md defines the executed command as Entrypoint with Cmd appended as its arguments, so an
// image with only Cmd starts and an image with only Entrypoint starts, while an image with neither
// has nothing to run. A consumer reading either field on its own would refuse a startable image or
// admit an unstartable one; the concatenation is the fact, and it is modelled once here rather
// than re-derived by every consumer.
fn image_config_start_command(c: ImageConfiguration) -> List<String> {
append(image_config_entrypoint(c: c), items: image_config_cmd(c: c))
}

// Same defect as image_config_entrypoint above, repaired together rather than left for the next
// consumer to rediscover: it is one class in one file, and fixing only the arm this change happens
// to call would leave a known-broken sibling behind.
fn image_config_first_exposed_port(c: ImageConfiguration) -> ContainerExposedPort? {
match c.config {
null => null
cfg =>
Absent => none
Present { value: cfg } =>
match cfg.ExposedPorts {
null => null
ports =>
match ports |> get(0) {
null => null
port => port
}
Absent => none
Present { value: ports } => ports |> get(0)
}
}
}
Expand All @@ -92,8 +121,9 @@ fn image_config_has_exposed_port(
expected_port: Int,
protocol: ContainerPortProtocol,
) -> Bool {
match image_config_first_exposed_port(c) {
null => false
port => container_exposed_port_is(port: port, expected_port: expected_port, protocol: protocol)
match image_config_first_exposed_port(c: c) {
Absent => false
Present { value: port } =>
container_exposed_port_is(port: port, expected_port: expected_port, protocol: protocol)
}
}
Loading
Loading