{"id":"a30b74fb-70c3-4db7-b4f6-e1bbb65422eb","arxiv_id":"1908.04502","paper_version":1,"verdict":"REJECT","confidence":"HIGH","novelty_score":2.0,"correctness_risk":"high","formal_verification":"none","parameter_count":0,"one_line_summary":"A stack-based path canonicalization routine is presented as a directory traversal defense, with a correctness proof that does not hold under the paper's own stated limitations.","lead":"The paper proposes a small stack-based algorithm that canonicalizes user-supplied file paths by resolving '.' and '..' tokens, then checks the result against a whitelist to block directory traversal attacks. It also offers a proof of correctness and a symbolic-execution verification strategy, but the proof and theorem overstate the safety guarantee.","discovery_kind":"incremental","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 1 is false as stated: the paper's own Section V.B counterexamples show sanitize accepts paths the filesystem rejects, so the iff claim about file identity does not hold.","rationale":"The reader's weakest_assumption correctly identifies the divergence between syntactic resolution and filesystem semantics as the key unsecured premise. The paper's own Section V.B provides concrete admissions of this divergence, making the issue internally acknowledged rather than an external point of contention. The theorem's 'if and only if' claim is the entire security argument: if sanitize accepts a path that the filesystem would not resolve to the whitelisted file, then an implementation that passes the sanitized path to a system call may behave in unanticipated, potentially security-relevant ways. The dismissal in Section V.B ('these improper directory traversal semantics do not pose problems') is unconvincing because the theorem is stated unconditionally for all path strings, and a defensive layer should not silently accept paths that the underlying filesystem rejects. The proof's forward direction adds no security content beyond string equality, so even if the proof were structurally complete, it would not establish the claimed filesystem identity. The symbolic-execution verification is also bounded and checks only syntactic properties such as absence of traversal tokens in the output, so it cannot rescue the semantic claim. Therefore the central claim is not supported, and the reader's REJECT verdict is appropriate. No new objection beyond the reader's is needed; the concern is load-bearing and already fatal to the paper's main theorem.","tokens_in":9087,"tokens_out":3407,"duration_ms":32325,"concrete_test":"Build a small harness that calls sanitize on the paper's own counterexamples and then checks filesystem resolution. 1) Call sanitize(\"/home/NonexistentUserFolder/../ActualUserFolder/\", [\"/home/ActualUserFolder/\"]) and verify it returns true, then call stat() or realpath() on the original path and confirm the filesystem returns ENOENT. 2) Call sanitize(\"/etc/passwd/./\", [\"/etc/passwd\"]) and verify it returns true, then attempt to open or stat \"/etc/passwd/./\" and confirm the filesystem rejects it (ENOTDIR or ENOENT). If either sanitize returns true while filesystem resolution fails, Theorem 1's forward direction is falsified.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central security guarantee is Theorem 1: sanitize(S1, [S2]) is true if and only if S1 and S2 refer to the same file. This requires that the algorithm's syntactic normalization exactly matches the operating system's path resolution. The paper itself, in Section V.B, gives two direct counterexamples: \"/home/NonexistentUserFolder/../ActualUserFolder/\" is accepted by sanitize and canonicalized to \"/home/ActualUserFolder/\", but the filesystem rejects the original path because the intermediate directory does not exist; and \"/etc/passwd/./\" is accepted (the \"/./\" is ignored), but the filesystem rejects it because \"/etc/passwd\" is a regular file, not a directory. In both cases sanitize(S1, [S2]) can return true for a path string S1 that does not refer to the same file as S2 — indeed S1 refers to no file at all. Thus the forward direction of Theorem 1 is false. The proof's forward direction is also not about filesystem identity: it merely restates that if the whitelist contains S2 and the algorithm's output equals S2, then the strings are equal, which is a tautology about string containment and says nothing about filesystem semantics. The paper dismisses these semantic divergences in Section V.B as not posing problems, but they are exactly what a directory traversal defense must handle: if a sanitized path is passed to a filesystem operation, the filesystem's own resolution rules determine what is actually accessed, and a mismatch can lead to security-relevant behavior that the algorithm's guarantee does not cover. This load-bearing flaw invalidates the claimed 'if and only if' theorem and with it the paper's central correctness argument.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a stack-based algorithm, 'sanitize', that tokenizes a user-supplied path string, resolves '.' and '..' tokens, and returns true if the resulting canonical string is contained in a whitelist of allowed path strings. The authors claim this provides a portable, lightweight, and easily verifiable defense against directory traversal attacks, and they support the claim with a proof of correctness (Theorem 1, an if-and-only-if statement about file identity) and with symbolic-execution experiments using KLEE. The paper also surveys existing mitigations (character removal, canonicalization, whitelisting) and argues that the new algorithm combines the benefits of whitelisting and syntactic canonicalization while avoiding filesystem calls.","tokens_in":9434,"tokens_out":6870,"duration_ms":68688,"significance":"If Theorem 1 were true, the algorithm would indeed be a useful building block: it is simple, self-contained, and amenable to formal verification, and the paper deserves credit for attempting a proof and for shipping reproducible verification artifacts (KLEE runs and a GitHub implementation). However, the central if-and-only-if claim is false as stated, and the paper's own Section V.B provides counterexamples that the authors dismiss without adequate justification. Because the security guarantee rests entirely on Theorem 1, the significance of the contribution as presented is not established. The symbolic-execution checks are limited to a bounded string length and do not verify the theorem's file-identity semantics.","major_comments":[{"comment":"The forward direction of Theorem 1 is false, and the paper's own Section V.B supplies the counterexamples. For S1 = '/home/NonexistentUserFolder/../ActualUserFolder/' and S2 = '/home/ActualUserFolder/', sanitize(S1, [S2]) returns true because the token 'NonexistentUserFolder' is popped by the following '..', yet the filesystem cannot resolve S1 because the intermediate directory does not exist. Similarly, S1 = '/etc/passwd/./' is accepted even though the filesystem rejects a path that treats a regular file as a directory. In both cases S1 does not refer to the same file as S2 (indeed, S1 refers to no file), contradicting the claim that sanitize(S1, [S2]) is true if and only if S1 and S2 refer to the same file. The proof of (⇒) only shows that the algorithmic output string equals S2; it does not bridge the gap between the output string and filesystem semantics.","section":"§III.A (Theorem 1)"},{"comment":"Lemma 2 is stated without a rigorous proof; the sentence 'This follows from the assumptions...' is an assertion, not a derivation, and it is not obvious why the length inequality must hold for every pair of path strings that denote the same file, especially when '..' tokens cross non-existent or non-directory components. Lemma 3's Case 2 relies on an informal red/green coloring argument and asserts that every 'red' directory must be popped by a later '..', but this is exactly the invariant that needs a formal inductive proof. The subsequent case analysis in Theorem 1's backward direction also never analyzes the situation where the stack is empty and a '..' token is silently discarded at the root; this interacts with the prefix invariant in a way the proof does not address.","section":"§III.A (Lemma 2 and Lemma 3)"},{"comment":"The paper acknowledges in Section V.B that sanitize 'does not process path strings in the same way as most operating systems or file systems' and then asserts that the resulting mismatches 'do not pose problems' because whitelisted path strings are valid. This assertion is not justified. The algorithm returns only a boolean, so a secure application must obtain the canonicalized string elsewhere for the actual file operation; the paper does not specify this usage or analyze the consequences of the application instead using the original user-supplied path after sanitize returns true. The acknowledged mismatches directly invalidate the theorem's file-identity claim, regardless of whether they constitute an exploit, because the theorem is stated about filesystem reference, not about string containment.","section":"§III.A and §V.B"},{"comment":"The algorithm treats relative path tokens as though they were rooted at '/', but the paper never states an explicit input assumption that user-supplied path strings are absolute. Definition 1 defines path strings as absolute, but the assumptions paragraph in Section III mentions only symbolic links and wildcards. If an implementation applies sanitize to a relative path such as 'a/b/c', the stack becomes '/a/b/c' and may be accepted by a whitelist containing '/a/b/c', even though the application would resolve the relative path against some current working directory. The absolute-path requirement needs to be stated prominently, and the security consequences of violating it need to be discussed.","section":"§III (assumptions)"}],"minor_comments":[{"comment":"The symbolic-execution verification uses strings of length at most 12 and single-letter directory names; the paper claims this is 'an effective and equivalent way' to represent longer paths, but no formal equivalence argument is given, and the experiments verify only that certain traversal tokens do not appear in the output and that a particular output string is enumerable, not the full if-and-only-if claim of Theorem 1.","section":"§IV"},{"comment":"In Algorithm 2, the loop condition 'for i← 0 to s.size' combined with 'result.append(s.data[i])' appears to access s.data[s.size] on the final iteration, which is out of bounds in a 0-indexed array; the pseudocode should clarify the intended bounds and indexing convention.","section":"§III (Algorithm 2)"},{"comment":"The footnote and Figure 3 caption contain typographical inconsistencies ('mini httpd' vs. 'mini_httpd', 't httpd'), and several references have URLs with unescaped spaces (e.g., [1]); these presentational issues should be cleaned up before any revised submission.","section":"§II.C.1"},{"comment":"The proof of Theorem 1 contains several wording glitches, including 'contain smethod' and 'S2a re allowed', and the proof's forward direction repeatedly refers to S1 after canonicalization as if it were the original input string, which obscures the distinction between the input string and the algorithm's output.","section":"§III.A"}],"recommendation":"reject","confidential_remarks":"The manuscript's central theorem is false as stated, and the authors' own Section V.B contains the counterexamples. I would not send this back for major revision unless the authors are willing to restate the security claim as a statement about the algorithm's output string (or about a canonicalized string that the application must use), provide a formal model of filesystem path resolution, and rework Lemmas 2 and 3 into a genuine inductive proof. The symbolic-execution work is a nice start but does not cover the missing semantic argument. The paper is also somewhat underdeveloped for a journal venue; it reads more like a short workshop paper."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The headline is that this paper is a well-written description of a very old algorithm. The stack-based removal of '.' and '..' with a whitelist check is essentially RFC 3986's remove_dot_segments, or Go's path.Clean, and the paper does not cite either. What is genuinely good: the exposition is clear, the no-symlink assumption is stated explicitly rather than hidden, and the KLEE verification exercises are a nice practical touch that would make the routine easy to regression-test.\n\nThe soft spot is load-bearing. Theorem 1 claims sanitize(S1,[S2]) is true iff S1 and S2 refer to the same file on the filesystem. That is false as stated, and the paper's own Section V.B admits it. '/home/NonexistentUserFolder/../ActualUserFolder/' is accepted by sanitize but the filesystem rejects it, so S1 refers to no file at all while sanitize returns true. The same holds for '/etc/passwd/./'. The proof of the forward direction is essentially a tautology about string containment, not about filesystem identity, and the reverse direction leans on the unproved Lemma 2. The proof also hand-waves the empty-stack case at the root, where '..' is silently discarded.\n\nThe author waves off the semantic divergences as 'not posing problems' because the whitelist only contains valid paths, but that misses the point: if the sanitized string is handed to a filesystem call, the filesystem's own resolution rules determine what is actually opened, and the algorithm's guarantee does not cover those rules. So the central correctness claim does not hold.\n\nFor all that, the paper is honestly written and the limitations are at least acknowledged. It could serve as a useful practitioner note about a simple defense layer, provided you enforce absolute paths, disallow symlinks, and accept that the syntactic canonicalization may diverge from the OS. As a research contribution it is not new, and the main theorem is false.\n\nMy call: this deserves a serious referee because the proof attempt, the shipped code, and the symbolic-execution runs give enough substance to engage with, but the outcome should be rejection unless the author reframes the contribution and drops the if-and-only-if claim. I would not cite it, but I would bring it to a reading group as a cautionary example of why syntactic normalization is not the same as filesystem semantics.","headline":"A clean write-up of a standard path-normalization routine whose central equivalence theorem is false as stated, admitted by the paper's own Section V.B.","tokens_in":9951,"tokens_out":2147,"would_cite":false,"duration_ms":20263,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper proposes a stack-based path canonicalizer that admits a user path only if its resolved form is whitelisted, claiming this is a portable, verifiable defense against directory traversal attacks.","keywords":["directory traversal","path traversal","path canonicalization","whitelisting","stack-based algorithm","web application security","symbolic execution"],"falsifier":"Run sanitize(\"/home/NonexistentUserFolder/../ActualUserFolder/\", [\"/home/ActualUserFolder/\"]) ; it returns true while the operating system reports that the first path does not exist, so the claimed if-and-only-if relationship with the filesystem fails for a concrete input.","tokens_in":8837,"feed_emoji":"🛡️","tokens_out":13232,"duration_ms":111434,"temperature":0.7,"pith_summary":"Directory traversal attacks let a malicious path like ../../etc/passwd escape the intended root, and existing mitigations—removing traversal characters, whitelisting, or filesystem canonicalization—are hard to verify or not cross-platform. This paper proposes sanitize, a short stack-based routine that tokenizes a user-supplied path, silently drops . tokens, pops the stack on .., and then checks whether the resulting string is in a whitelist. The paper's central claim is Theorem 1: under the assumptions of no symbolic links and a canonicalized whitelist, sanitize(S1, [S2]) returns true precisely when S1 and S2 name the same file on the filesystem. If that claim holds, developers get a defense that is tiny, portable, and amenable to exhaustive symbolic-execution verification, which the paper demonstrates by enumerating all bounded-length inputs that reach a whitelisted path and finding no traversal tokens in the output.","feed_headline":"Stack algorithm collapses paths to block traversal attacks","feed_subtitle":"A tiny routine canonicalizes any path into one string, then checks it against a whitelist—small and verifiable.","key_machinery":"The load-bearing object is Algorithm 1 (sanitize), a stack machine for path strings: tokenize on the slash separator, push ordinary tokens, skip . tokens, and on .. either pop the stack or, if the stack is empty, drop the token. Its companion toString method reconstitutes the canonical path as a slash-joined string, which is then checked against the whitelist with an array contains operation. The central identity is Theorem 1, which ties the stack's final contents to filesystem reference equality under the no-symlink, canonicalized-whitelist assumptions. The stack's behavior is the entire mechanism; there is no filesystem access, no symlink resolution, and no unbounded loop beyond the input length.","core_discovery":"The central discovery is that directory traversal defense can be reduced to a pure string-collapsing operation: treat every path as a stack of directory names, where . is a no-op and .. pops the current top, then compare the resulting canonical string against a whitelist. The stack is entirely in memory, never touching the filesystem, which makes the routine cross-platform and free of symlink-resolution pitfalls if whitelist entries are canonical and symlink-free. The paper proves Theorem 1 to establish the soundness and completeness of this comparison, and reports that symbolic execution over all strings of length up to 12 finds no output containing /../ or /./, supporting the claim that no traversal token survives canonicalization.","pith_inferences":["A corrected variant could push a root sentinel onto the stack before processing, so a leading .. at the root pops the sentinel instead of being silently discarded; that would align the algorithm with POSIX resolution while preserving the rest of the machinery.","The same stack collapse could be extended to case-insensitive or mount-aware filesystems by adding a normalization step before the final contains check, though the paper does not address those environments.","If the final check were changed from exact string equality to prefix or wildcard matching, the algorithm would lose its correctness guarantee; an implementer wanting wildcards would need a new theorem."],"forward_implications":["Whitelist maintenance becomes tractable: infinitely many path spellings of one file all reduce to a single canonical string, so a small, static whitelist can govern access.","Verification is practical enough for regression testing: exhaustive symbolic execution over bounded input lengths runs in minutes and finds no traversal tokens in the output.","The routine ports to any language with a stack container and requires no system calls, making it usable in sandboxed or minimal web-application environments.","When the algorithm accepts a path the filesystem later rejects, the actual I/O fails closed; the paper contends this does not weaken the defense because whitelisted entries are valid paths."],"supporting_citations":[{"why":"supplies the de dotdot routine the paper analyzes as a semantically flawed traversal-removal approach.","marker":"[9]"},{"why":"serves as the second implementation sharing that flawed routine and its associated CVE context.","marker":"[10]"},{"why":"represents the realpath-style canonicalization approach the algorithm deliberately avoids by staying off the filesystem.","marker":"[12]"},{"why":"documents a real traversal vulnerability in the analyzed servers, motivating a testable defense.","marker":"[15]"},{"why":"provides the reference C implementation used in the paper's symbolic-execution verification runs.","marker":"[16]"},{"why":"is the symbolic execution engine used to exhaustively enumerate all length-12-or-less input strings.","marker":"[18]"}],"fun_headline_variants":["Stack-based path collapsing blocks directory traversal","Tidy stack algorithm prevents path traversal attacks","Collapse paths with a stack to outsmart traversal bugs","One small stack routine neutralizes traversal attempts","A simple stack routine canonicalizes paths to block traversal"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that a purely textual collapse of . and .. matches the operating system's own path resolution for every path that reaches the whitelist check, including the existence of intermediate directories and the behavior of .. at the root.","fun_headline_variants_meta":{"raw":{"variants":["Stack-based path collapsing blocks directory traversal","Tidy stack algorithm prevents path traversal attacks","Collapse paths with a stack to outsmart traversal bugs","One small stack routine neutralizes traversal attempts","A simple stack routine canonicalizes paths to block traversal"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000769,"raw_usage":{"total_tokens":3355,"prompt_tokens":841,"completion_tokens":2514,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":457,"completion_tokens_details":{"reasoning_tokens":2444}},"tokens_in":457,"tokens_out":2514,"duration_ms":19607,"temperature":1.0,"reasoning_tokens":2444,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T13:40:43.422268+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run sanitize(\"/home/NonexistentUserFolder/../ActualUserFolder/\", [\"/home/ActualUserFolder/\"]) ; it returns true while the operating system reports that the first path does not exist, so the claimed if-and-only-if relationship with the filesystem fails for a concrete input.","supporting_citations":[{"cited_title":"[Online]","cited_arxiv_id":null,"evidence_quote":"supplies the de dotdot routine the paper analyzes as a semantically flawed traversal-removal approach."},{"cited_title":"[Online]","cited_arxiv_id":null,"evidence_quote":"serves as the second implementation sharing that flawed routine and its associated CVE context."},{"cited_title":"realpath","cited_arxiv_id":null,"evidence_quote":"represents the realpath-style canonicalization approach the algorithm deliberately avoids by staying off the filesystem."},{"cited_title":"(2018, 10) CVE-2018-18778 Details","cited_arxiv_id":null,"evidence_quote":"documents a real traversal vulnerability in the analyzed servers, motivating a testable defense."},{"cited_title":"sanitize,","cited_arxiv_id":null,"evidence_quote":"provides the reference C implementation used in the paper's symbolic-execution verification runs."}],"review_version":1}