lean_ctx/core/
pathjail_write.rs

1// SPDX-License-Identifier: Apache-2.0
2//! Write destinations below a trusted root that refuse symlinked components.
3//!
4//! Project data (`<project>/.lean-ctx/...`) lives inside a working tree that
5//! other people, checkouts and tools can populate. A symlinked `.lean-ctx`,
6//! `proofs` or target file there must not redirect a LeanCTX write outside the
7//! project, so these writes rebuild the path component by component below the
8//! trusted root and fail closed on any link. The mechanics (directory handles,
9//! `O_NOFOLLOW`, `renameat`) live in [`lean_ctx_fs::confined_write`].
10
11use std::path::{Path, PathBuf};
12
13const PROJECT_DATA_DIR: &str = ".lean-ctx";
14
15/// Rebuild `root/rel` component by component, refusing every symlinked
16/// component below `root` (a check only; nothing is created).
17pub fn rebuild_below(root: &Path, rel: &Path) -> Result<PathBuf, String> {
18    lean_ctx_fs::confined_write::rebuild_below(root, rel).map_err(|e| e.to_string())
19}
20
21/// Write `content` to `root/rel` (file `mode` on Unix), creating missing
22/// directories, without following a symlink anywhere below `root`.
23///
24/// Only the symlink boundary is enforced here; whether `root` may be written
25/// at all (read-only roots, jail scope) stays the caller's policy.
26pub fn write_below(root: &Path, rel: &Path, content: &[u8], mode: u32) -> Result<PathBuf, String> {
27    lean_ctx_fs::confined_write::write_below(root, rel, content, mode).map_err(|e| e.to_string())
28}
29
30/// The relative path below the project root for `rel` inside the project's
31/// data directory, after the data-dir collision check.
32fn project_data_rel(project_root: &Path, rel: &Path) -> Result<PathBuf, String> {
33    crate::core::pathutil::safe_project_data_dir(project_root)?;
34    Ok(Path::new(PROJECT_DATA_DIR).join(rel))
35}
36
37/// Check a destination `<project>/.lean-ctx/<rel>` without writing it.
38pub fn project_data_destination(project_root: &Path, rel: &Path) -> Result<PathBuf, String> {
39    rebuild_below(project_root, &project_data_rel(project_root, rel)?)
40}
41
42/// Write `<project>/.lean-ctx/<rel>`: the project root is trusted, `.lean-ctx`
43/// and everything below it must not be a symlink.
44pub fn write_project_data(
45    project_root: &Path,
46    rel: &Path,
47    content: &[u8],
48) -> Result<PathBuf, String> {
49    write_below(
50        project_root,
51        &project_data_rel(project_root, rel)?,
52        content,
53        0o600,
54    )
55}
56
57/// `path` as plain components below `root`: lexically first (so a symlinked
58/// component stays visible and is refused), then against the canonical root
59/// for a caller that already resolved it.
60pub fn relative_below(root: &Path, path: &Path) -> Result<PathBuf, String> {
61    let plain = |rel: &Path| {
62        rel.components()
63            .all(|c| matches!(c, std::path::Component::Normal(_)))
64            && rel.components().next().is_some()
65    };
66    if let Ok(rel) = path.strip_prefix(root)
67        && plain(rel)
68    {
69        return Ok(rel.to_path_buf());
70    }
71    let canonical_root = crate::core::pathutil::canonicalize_secure_or_self(root);
72    match path.strip_prefix(&canonical_root) {
73        Ok(rel) if plain(rel) => Ok(rel.to_path_buf()),
74        _ => Err(format!(
75            "{} is not below {}",
76            path.display(),
77            root.display()
78        )),
79    }
80}
81
82/// Write a caller-chosen destination below `root`: the lexical `requested`
83/// path when it names plain components below `root` (a symlinked component
84/// then stays visible and is refused), else the jail-resolved `jailed` path.
85///
86/// A `jailed` path outside `root` (an extra jail root the user allowed, or a
87/// disabled jail) keeps working: its parent directory, which the jail already
88/// resolved, is the trusted root and only the file itself must not be a link.
89pub fn write_requested_below(
90    root: &Path,
91    requested: &Path,
92    jailed: &Path,
93    content: &[u8],
94) -> Result<PathBuf, String> {
95    if let Ok(rel) = relative_below(root, requested).or_else(|_| relative_below(root, jailed)) {
96        return write_below(root, &rel, content, 0o600);
97    }
98    let (Some(parent), Some(name)) = (jailed.parent(), jailed.file_name()) else {
99        return Err(format!("invalid destination: {}", jailed.display()));
100    };
101    std::fs::create_dir_all(parent).map_err(|e| format!("{}: {e}", parent.display()))?;
102    write_below(parent, Path::new(name), content, 0o600)
103}
104
105#[cfg(all(test, unix))]
106mod tests {
107    use super::*;
108    use std::os::unix::fs::symlink;
109
110    #[test]
111    fn project_data_writes_land_in_the_project() {
112        let project = tempfile::tempdir().unwrap();
113        let path = write_project_data(project.path(), Path::new("proofs/a.json"), b"{}").unwrap();
114        assert_eq!(path, project.path().join(".lean-ctx/proofs/a.json"));
115        assert_eq!(std::fs::read(&path).unwrap(), b"{}");
116    }
117
118    #[test]
119    fn a_symlinked_data_dir_pointing_outside_is_refused() {
120        let tmp = tempfile::tempdir().unwrap();
121        let project = tmp.path().join("project");
122        let outside = tmp.path().join("outside");
123        std::fs::create_dir_all(&project).unwrap();
124        std::fs::create_dir_all(&outside).unwrap();
125        symlink(&outside, project.join(".lean-ctx")).unwrap();
126        let err = write_project_data(&project, Path::new("proofs/a.json"), b"x").unwrap_err();
127        assert!(err.contains("symlink"), "{err}");
128        assert!(!outside.join("proofs").exists());
129    }
130
131    #[test]
132    fn relative_below_keeps_links_visible() {
133        let tmp = tempfile::tempdir().unwrap();
134        let root = tmp.path().join("r");
135        std::fs::create_dir_all(&root).unwrap();
136        assert_eq!(
137            relative_below(&root, &root.join("a/b")).unwrap(),
138            PathBuf::from("a/b")
139        );
140        assert!(relative_below(&root, &tmp.path().join("x")).is_err());
141    }
142}
lean_ctx/core/pathjail_write.rs

lean_ctx/core/
pathjail_write.rs
