Skip to content
27 changes: 27 additions & 0 deletions dag/extdeps/os/exec_arg_limit.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
module extdeps.os.exec_arg_limit

import std.measure { ByteSize, byte_size, byte_size_count }
import std.types { String }
import extdeps.external_authority { ExternalAuthority }
import extdeps.uri { Uri, Https }
import extdeps.runtime.architecture.x86_64_linux { x86_64_linux_architecture_profile }

data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
uri: Uri {
scheme: Https
locator: "man7.org/linux/man-pages/man2/execve.2.html"
}
}

data linux_execve_max_arg_strlen_page_factor: Nat = 32

fn host_exec_arg_max_strlen_from_page(page: ByteSize, page_factor: Nat) -> ByteSize {
byte_size(count: byte_size_count(page) * page_factor)
}

data host_exec_arg_max_strlen: ByteSize = host_exec_arg_max_strlen_from_page(
page: x86_64_linux_architecture_profile.page_size,
page_factor: linux_execve_max_arg_strlen_page_factor,
)

data host_exec_arg_max_strlen_note: String = "Linux execve(2) per-argument ceiling: MAX_ARG_STRLEN = linux_execve_max_arg_strlen_page_factor (32) * PAGE_SIZE. host_exec_arg_max_strlen is DERIVED from extdeps.runtime.architecture.x86_64_linux.page_size — not an independent 131072 literal. A single argv or envp string longer than this makes execve fail with E2BIG (\"Argument list too long\") — the opaque os error 7 the srv1 deploy hit when a >128KB script was embedded in one sh -c argv element. Distinct from ARG_MAX (~2 MiB total argv+envp; getconf ARG_MAX) — not modeled here (using MAX_ARG_STRLEN as ARG_MAX would be an over-approximation, §5). Consumer seam: extdeps.shell shell.Exec.Check embeds the command input as one argv token (sh -c); shell.Exec.Run routes payload via stdin (sh -s) and does not hit this ceiling. The v1 interpreter shell dispatch (dispatch_shell) realizes the wall: refuse with InterpError::ArgvExceedsHostArgMax before spawn. Part A (route deploy scripts through Run/stdin) is #6711; this authority is the general host-boundary guard for every remaining argv-embedding site."
16 changes: 7 additions & 9 deletions dag/extdeps/shell/shell.dag
Original file line number Diff line number Diff line change
@@ -1,9 +1,10 @@
module extdeps.shell

import std.types { FilePath, NonEmptyStr }
import std.measure { ByteSize, byte_size }
import std.types { FilePath, NonEmptyStr, String }
import std.measure { ByteSize }
import extdeps.external_authority { ExternalAuthority }
import extdeps.uri { Uri, Https }
import extdeps.os.exec_arg_limit { host_exec_arg_max_strlen }

data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
uri: Uri {
Expand All @@ -12,14 +13,11 @@ data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
}
}

data extdeps_shell_argv_strlen_authority: ExternalAuthority = ExternalAuthority {
uri: Uri {
scheme: Https
locator: "elixir.bootlin.com/linux/latest/source/include/uapi/linux/binfmts.h"
}
}
data shell_exec_run_stdin_route_note: String = "shell.Exec.Run transport: argv is fixed [sh, -s]; the script input is routed through the transport stdin field. Large payloads belong here — they never become a single argv token, so they do not encounter the Linux per-argument exec ceiling modeled in extdeps.os.exec_arg_limit.host_exec_arg_max_strlen (deploy Part A / #6711)."

data shell_exec_check_argv_embed_note: String = "shell.Exec.Check transport: argv is [sh, -c, command] — the entire command string is ONE argv element. On Linux hosts this is the surface that hits execve(2) MAX_ARG_STRLEN (extdeps.os.exec_arg_limit.host_exec_arg_max_strlen): an oversized embed fails E2BIG (opaque os error 7) unless the interpreter refuses first at dispatch_shell (InterpError::ArgvExceedsHostArgMax). Prefer Run for payloads approaching the per-argument ceiling."

data shell_argv_max_arg_strlen: ByteSize = byte_size(131072)
data shell_exec_transport_ceiling_authority: ByteSize = host_exec_arg_max_strlen

service shell.Find {
operation ListDirs {
Expand Down
45 changes: 45 additions & 0 deletions dag/test/claim/exec_arg_limit_witness_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
module test.claim.exec_arg_limit_witness

import std.types { Bool, String }
import std.measure { byte_size_count }
import extdeps.os.exec_arg_limit {
host_exec_arg_max_strlen,
host_exec_arg_max_strlen_from_page,
linux_execve_max_arg_strlen_page_factor,
}
import extdeps.runtime.architecture.x86_64_linux { x86_64_linux_architecture_profile }
import extdeps.runtime.architecture.aarch64_linux { aarch64_linux_architecture_profile }
import extdeps.filesystem.filesystem_io
import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree }

data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree

data exec_arg_limit_witness_note: String = "Single-authority closure for the Linux per-argument exec ceiling. host_exec_arg_max_strlen is derived (32 * PAGE_SIZE from x86_64_linux_architecture_profile); shell.Exec.Check is the argv-embedding consumer; dispatch_shell in v1_interpreter realizes the typed refusal. witness_rust_const_mirrors_authority cross-checks the Rust seed const against the derived authority; argv_arg_limit_test::dispatch_shell_wiring_refuses_oversized_argv proves the dispatch path in-crate."

data v1_interpreter_source_path: String = "src/v1/stage0/src/v1_interpreter.rs"

fn witness_host_exec_arg_max_strlen_is_execve_formula() -> Bool {
host_exec_arg_max_strlen == host_exec_arg_max_strlen_from_page(
page: x86_64_linux_architecture_profile.page_size,
page_factor: linux_execve_max_arg_strlen_page_factor,
)
}

fn witness_linux_page_size_uniform_on_deploy_architectures() -> Bool {
byte_size_count(x86_64_linux_architecture_profile.page_size) == byte_size_count(aarch64_linux_architecture_profile.page_size)
}

fn witness_rust_const_mirrors_authority() -> Bool {
let src = filesystem_read(path: v1_interpreter_source_path)
let expected = to_string(byte_size_count(b: host_exec_arg_max_strlen))
string_contains(
s: src.content,
pattern: concat("HOST_ARG_MAX_STRLEN_BYTES: usize = ", concat(expected, ";")),
)
}

test fn exec_arg_limit_witnesses() -> Bool {
witness_host_exec_arg_max_strlen_is_execve_formula()
&& witness_linux_page_size_uniform_on_deploy_architectures()
&& witness_rust_const_mirrors_authority()
}
4 changes: 2 additions & 2 deletions dag/test/claim/shell_exec_run_argv_embed_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ import std.measure { byte_size_count }
import gunbc.live_deploy.emit { live_deploy_apply_script_for }
import gunbc.live_deploy.spec { deployment_spec_srv1 }
import extdeps.filesystem.filesystem_io
import extdeps.shell { shell_argv_max_arg_strlen }
import extdeps.os.exec_arg_limit { host_exec_arg_max_strlen }
import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree }

data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree
Expand All @@ -19,7 +19,7 @@ fn src_has(path: String, needle: String) -> Bool {

fn witness_apply_script_exceeds_local_argv_embed_budget() -> Bool {
let script_len = length(live_deploy_apply_script_for(spec: deployment_spec_srv1()))
let budget = byte_size_count(b: shell_argv_max_arg_strlen)
let budget = byte_size_count(b: host_exec_arg_max_strlen)
script_len > budget
}

Expand Down
4 changes: 2 additions & 2 deletions dag/test/claim/ssh_transport_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ import std.types { Bool, NonEmptyStr }
import std.measure { byte_size_count }
import gunbc.live_deploy.emit { live_deploy_apply_script_for }
import gunbc.live_deploy.spec { deployment_spec_srv1 }
import extdeps.shell { shell_argv_max_arg_strlen }
import extdeps.os.exec_arg_limit { host_exec_arg_max_strlen }
import extdeps.diagnostic.mock_corpus { diagnostic_ssh_session_mock_case_exec_script }
import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }

Expand All @@ -14,7 +14,7 @@ data ssh_exec_script_remote_receiver: NonEmptyStr = "bash -s"

fn witness_apply_script_exceeds_argv_embed_budget() -> Bool {
let script_len = length(live_deploy_apply_script_for(spec: deployment_spec_srv1()))
let budget = byte_size_count(b: shell_argv_max_arg_strlen)
let budget = byte_size_count(b: host_exec_arg_max_strlen)
script_len > budget
}

Expand Down
Loading
Loading