strict-path 0.1.2

Handle paths from external or unknown sources securely. Defends against 19+ real-world CVEs including symlinks, Windows 8.3 short names, and encoding tricks and exploits.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50

#[cfg(kani)]
mod verification {
    #[derive(Copy, Clone, Debug, kani::Arbitrary)]
    enum MockComponent {
        Normal,
        CurDir,
        ParentDir,
        RootDir,
        Prefix,
    }

    fn virtualize(components: &[MockComponent]) -> Vec<MockComponent> {
        let mut parts = Vec::new();
        for comp in components {
            match comp {
                MockComponent::Normal => parts.push(MockComponent::Normal),
                MockComponent::CurDir => {}
                MockComponent::ParentDir => {
                    if parts.pop().is_none() {
                        // At virtual root; ignore extra ".."
                    }
                }
                MockComponent::RootDir | MockComponent::Prefix => {
                    parts.clear();
                }
            }
        }
        parts
    }

    #[kani::proof]
    #[kani::unwind(10)]
    fn verify_virtualize_clamping() {
        // Use a fixed-size array instead of Vec to work with Kani's Arbitrary trait
        let components: [MockComponent; 8] = kani::any();

        let result = virtualize(&components);

        // Property: The result should only contain Normal components.
        // This proves that the virtualization logic effectively strips all
        // traversal (ParentDir), root resets (RootDir/Prefix), and no-ops (CurDir),
        // leaving only a safe relative path.
        for comp in &result {
            match comp {
                MockComponent::Normal => {}
                _ => panic!("Result contained non-Normal component: {:?}", comp),
            }
        }
    }
}