Build depends on SNAPSHOT artifacts and non-enforced version locks

Đang mở
  • Có gì không ổn?
#4,971 0 bình luận 0 reaction 0 người được giao Xem trên GitHub

Chưa có ai nhận issue này.

Đánh giá

Độ khó
4/5
Thời gian dự kiến
3-5 ngày
Mức phù hợp với người mới
22/100
Loại issue
Tái cấu trúc
Độ rõ ràng
Cần làm rõ
Mức độ hoạt động
Sôi nổi
Công nghệ
java
Lĩnh vực
build-system, security

Hướng nghiên cứu

Start with the parent pom.xml (repository and pluginRepository blocks near lines 36-54) and k-frontend/pom.xml (the nailgun-server and ng dependencies near lines 157 and 169), then compare them with the lock files under mvn-lock/ and the k-lock target in nix/k.nix and flake.nix. Done would mean the build resolves only pinned release artifacts, or enforces the lock in the plain Maven path, with maintainers agreeing on the approach first. The issue itself leaves the fix undecided, so confirm the direction before writing code.

Do mô hình lập chỉ mục viết ra từ nội dung của issue.

Mô tả

Summary

k-frontend/pom.xml consumes 1.0.0-k5.0-SNAPSHOT artifacts from the RV Maven repository; a rebuilt SNAPSHOT changes the toolchain without any repo change.

4 finding(s) (2 MEDIUM, 2 LOW) — line-anchor verified at commit 4a46d1231473.

Findings
Severity ID Location Summary
MEDIUM supply-chain-build-007 pom.xml:197 Maven dependency locks exist but are not enforced by the POM build
MEDIUM supply-chain-build-008 k-frontend/pom.xml:169 Native executable ng pulled as a 1.0.0-k5.0-SNAPSHOT Maven artifact
LOW supply-chain-build-006 pom.xml:36 Maven SNAPSHOT repository enabled for the whole build
LOW supply-chain-build-009 k-frontend/pom.xml:157 nailgun-server:1.0.0-SNAPSHOT resolved from a third-party repository
Details
supply-chain-build-007 — Maven dependency locks exist but are not enforced by the POM build (pom.xml:197)

Trigger (as reviewed): mvn-lock//dependencies-lock.json files (with sha512 integrity fields for every artifact) are checked in, and nix/k.nix / flake.nix only generate them (the k-lock attribute runs dependency-lock-maven-plugin:1.2.2:lock). Grepping the POMs for dependency-lock / dependencies-lock finds no binding the plugin's verify/check goal to a lifecycle phase. Consequently mvn package, as invoked by package/debian//rules.* and package/arch/PKGBUILD, resolves dependencies from remote repositories without consulting the lock.

Impact (as reviewed): The integrity data in mvn-lock/ provides no protection for the ordinary (non-Nix) build paths that produce the released .debs and Arch packages. A compromised or typosquatted artifact at a resolved coordinate is accepted; the checked-in lock is decorative in those paths. A partially applied verification gap: the repo looks locked but the enforcing step is absent.

Deep review: reachability=REACHABLE-FROM-UNTRUSTED; exploitability=EXPLOITABLE; red-team=RED-TEAM-SURVIVED.

Strongest counterargument found during red-teaming: The exploit requires an attacker with write access to runtimeverification.mycloudrepo.io, and the maintainers explicitly documented the lock as informational/best-effort in commit #4820. Whether that documented tradeoff should count as an accepted risk with an owner (lowering or closing this as a finding) is a judgment the code alone cannot settle; the external repository's redeploy/immutability policy for the 1.0.0-SNAPSHOT coordinates is also unverifiable from this checkout.

supply-chain-build-008 — Native executable `ng` pulled as a `1.0.0-k5.0-SNAPSHOT` Maven artifact (k-frontend/pom.xml:169)

Trigger (as reviewed): The frontend declares a uexe (native executable) dependency on org.kframework.dependencies:ng at a -SNAPSHOT version, with sibling declarations at 0.9.2-k4.0 for linux (line 161) and windows (line 175). The snapshot repository is enabled (see -006). ng/kserver are the nailgun launchers that the distribution executes (k-distribution/src/main/scripts/lib/checkJava invokes bin/ng), and k-distribution/src/main/assembly/bin.xml copies :uexe: artifacts into lib/kframework/bin.

Impact (as reviewed): An unverifiable, re-publishable native binary is bundled into the shipped distribution and executed on the user's machine. Maven's checksum check only proves consistency with whatever the repository currently serves for that snapshot coordinate, not that the binary is the reviewed one. Direct binary-supply-chain injection point into every K install.

Deep review: reachability=REACHABLE-FROM-UNTRUSTED; exploitability=EXPLOITABLE; red-team=RED-TEAM-INCONCLUSIVE.

Strongest counterargument found during red-teaming: The Nix fixed-output hash fully protects released macOS installations (the only shipped macOS channel) and Linux packages, so an artifact-repository-only attacker cannot reach end users; however the finding still survives in a narrower form: the README-documented mvn package developer build on macOS resolves the mutable snapshot fresh with no enforced digest (the lock file is only generated by the separate k-lock Nix output), and the build/tests plus the resulting local distribution execute lib/kframework/bin/ng, giving RCE on macOS build machines.

supply-chain-build-006 — Maven SNAPSHOT repository enabled for the whole build (pom.xml:36)

Trigger (as reviewed): The parent POM enables snapshot resolution from a third-party host (runtimeverification.mycloudrepo.io) for all modules. The same repository is registered again as a pluginRepository (lines 50-54), so build plugins can also be resolved as snapshots.

Impact (as reviewed): Snapshot artifacts are mutable by design: the same coordinates can be re-published with different bytes. Any module that resolves a -SNAPSHOT coordinate silently picks up re-published content on the next non-offline build. Because the repository is operator-controlled and not central, this is a persistent supply-chain path that survives normal dependency pinning.

supply-chain-build-009 — `nailgun-server:1.0.0-SNAPSHOT` resolved from a third-party repository (k-frontend/pom.xml:157)

Trigger (as reviewed): nailgun-server is a compile-scope dependency at a snapshot version, resolved from runtimeverification.mycloudrepo.io. The lock file records its sha512, but (per -007) the lock is not enforced in the plain Maven build. checkJava in the distribution uses the nailgun server socket (KSERVER_SOCKET, $NG --nailgun-server local:$KSERVER_SOCKET/socket), so this class is loaded into the long-running kserver process.

Impact (as reviewed): Mutable snapshot code runs in the compiler server process that K's tooling talks to. A re-published snapshot (or a repo compromise) substitutes new bytecode with no enforced hash and no signature; because it is compile-scope it also enters the toolchain's classpath at runtime.

Deep review: reachability=REACHABLE-FROM-UNTRUSTED; exploitability=EXPLOITABLE; red-team=RED-TEAM-SURVIVED.

Strongest counterargument found during red-teaming: The attack requires write access to Runtime Verification's own CloudRepo namespace (or a compromise of CloudRepo itself), and the repository is first-party rather than the 'third-party repository' the title claims. Whether CloudRepo permits adding new timestamped snapshots under that coordinate, and whether the release deploy job really executes the integration-test/kserver phase while MAVEN_PASSWORD is in the environment, could not be verified offline. These affect severity and framing, not the existence of the unenforced mutable-snapshot dependency.

Suggested fix

Publish/rely on release (not SNAPSHOT) artifacts for ng, nailgun-server, and mpfr_java, and enforce the dependency lock in CI so unexpected version changes fail the build.

From a static audit of this repository at commit 4a46d1231473b599c699160132fd6e76a5c46406 (master). Every location above was verified against the source at that revision; no exploit code was run against this repository or its infrastructure.

Ngôn ngữ chính
Python
Star
605
Fork
165
Không có pull request nào được merge trong 30 ngày

Chuẩn bị môi trường

Bắt đầu từ đâu

  1. Đọc hết issue, rồi đọc hướng dẫn đóng góp của dự án.
  2. Bình luận trên issue rằng bạn sẽ nhận — tránh hai người làm cùng một việc.
  3. Fork repository và làm thay đổi trên một nhánh.
  4. Mở pull request có tham chiếu số hiệu của issue.

Issue khác của runtimeverification/k

Tất cả issue của runtimeverification/k

Issue tương tự

Thêm issue về Python

Nhận issue mới trong hộp thư của bạn

Bản tóm tắt ngắn những issue GitHub phù hợp với người mới.