1"use strict";(self.webpackChunkhomepage=self.webpackChunkhomepage||[]).push([["3645"],{5004(e,n,i){i.r(n),i.d(n,{metadata:()=>t,default:()=>h,frontMatter:()=>o,contentTitle:()=>c,toc:()=>a,assets:()=>d});var t=JSON.parse('{"id":"concepts/spec-driven","title":"The Idea Behind Specification-Driven Auditing","description":"Limits of Code-Driven Tools","source":"@site/i18n/en/docusaurus-plugin-content-docs/current/concepts/spec-driven.md","sourceDirName":"concepts","slug":"/concepts/spec-driven","permalink":"/en/docs/concepts/spec-driven","draft":false,"unlisted":false,"editUrl":"https://github.com/NyxFoundation/speca/tree/dev/website/docs/concepts/spec-driven.md","tags":[],"version":"current","sidebarPosition":1,"frontMatter":{"sidebar_position":1},"sidebar":"tutorialSidebar","previous":{"title":"Phase 04: Review (3-Gate FP Filter)","permalink":"/en/docs/pipeline/review"},"next":{"title":"Proof-Attempt Based Auditing","permalink":"/en/docs/concepts/proof-attempt"}}'),s=i(4848),r=i(8453);let o={sidebar_position:1},c="The Idea Behind Specification-Driven Auditing",d={},a=[{value:"Limits of Code-Driven Tools",id:"limits-of-code-driven-tools",level:2},{value:"The Specification-Driven Approach",id:"the-specification-driven-approach",level:2},{value:"Advantages",id:"advantages",level:2}];function l(e){let n={a:"a",code:"code",h1:"h1",h2:"h2",header:"header",li:"li",ol:"ol",p:"p",strong:"strong",table:"table",tbody:"tbody",td:"td",th:"th",thead:"thead",tr:"tr",ul:"ul",...(0,r.R)(),...e.components};return(0,s.jsxs)(s.Fragment,{children:[(0,s.jsx)(n.header,{children:(0,s.jsx)(n.h1,{id:"the-idea-behind-specification-driven-auditing",children:"The Idea Behind Specification-Driven Auditing"})}),"\n",(0,s.jsx)(n.h2,{id:"limits-of-code-driven-tools",children:"Limits of Code-Driven Tools"}),"\n",(0,s.jsx)(n.p,{children:"Conventional security tools detect known bug patterns:"}),"\n",(0,s.jsxs)(n.ul,{children:["\n",(0,s.jsxs)(n.li,{children:["CWE-89: SQL injection (template: ",(0,s.jsx)(n.code,{children:'query = "SELECT * FROM users WHERE id=" + user_input'}),")"]}),"\n",(0,s.jsxs)(n.li,{children:["CWE-22: Path traversal (template: ",(0,s.jsx)(n.code,{children:"open(userpath)"})," without sanitize)"]}),"\n",(0,s.jsx)(n.li,{children:"Memory corruption, race conditions, etc."}),"\n"]}),"\n",(0,s.jsxs)(n.p,{children:["However, ",(0,s.jsx)(n.strong,{children:"in systems governed by a specification, vulnerabilities arise as violations of spec-level invariants"}),". They cannot be expressed by local pattern matching on code:"]}),"\n",(0,s.jsxs)(n.ul,{children:["\n",(0,s.jsx)(n.li,{children:'Cryptographic protocols: mathematical invariants such as "message authentication holds" or "independence of randomness"'}),"\n",(0,s.jsx)(n.li,{children:'State machines: requirements such as "in this state, transitioning to state X is forbidden"'}),"\n",(0,s.jsx)(n.li,{children:'Consensus: "verification of this block must always preserve a safety invariant"'}),"\n"]}),"\n",(0,s.jsx)(n.h2,{id:"the-specification-driven-approach",children:"The Specification-Driven Approach"}),"\n",(0,s.jsx)(n.p,{children:"SPECA analyzes in the reverse direction:"}),"\n",(0,s.jsxs)(n.ol,{children:["\n",(0,s.jsxs)(n.li,{children:["\n",(0,s.jsx)(n.p,{children:(0,s.jsx)(n.strong,{children:"Derive typed properties from the specification"})}),"\n",(0,s.jsxs)(n.ul,{children:["\n",(0,s.jsx)(n.li,{children:"Invariant: a condition that must always hold"}),"\n",(0,s.jsx)(n.li,{children:"Precondition: a requirement before function execution"}),"\n",(0,s.jsx)(n.li,{children:"Postcondition: a guarantee after execution"}),"\n",(0,s.jsx)(n.li,{children:"Assumption: a dependency on an external system"}),"\n"]}),"\n"]}),"\n",(0,s.jsxs)(n.li,{children:["\n",(0,s.jsx)(n.p,{children:(0,s.jsx)(n.strong,{children:'Ask the implementation to "try to prove this property"'})}),"\n",(0,s.jsxs)(n.ul,{children:["\n",(0,s.jsx)(n.li,{children:"Proof gap = vulnerability candidate"}),"\n"]}),"\n"]}),"\n",(0,s.jsxs)(n.li,{children:["\n",(0,s.jsx)(n.p,{children:(0,s.jsx)(n.strong,{children:"Recall-safe FP filtering"})}),"\n",(0,s.jsxs)(n.ul,{children:["\n",(0,s.jsx)(n.li,{children:"3-gate review: Dead Code / Trust Boundary / Scope"}),"\n",(0,s.jsx)(n.li,{children:"Systematically reduces FPs while preserving the detection rate"}),"\n"]}),"\n"]}),"\n"]}),"\n",(0,s.jsx)(n.h2,{id:"advantages",children:"Advantages"}),"\n",(0,s.jsxs)(n.table,{children:[(0,s.jsx)(n.thead,{children:(0,s.jsxs)(n.tr,{children:[(0,s.jsx)(n.th,{children:"Aspect"}),(0,s.jsx)(n.th,{children:"Benefit"})]})}),(0,s.jsxs)(n.tbody,{children:[(0,s.jsxs)(n.tr,{children:[(0,s.jsx)(n.td,{children:(0,s.jsx)(n.strong,{children:"Detection"})}),(0,s.jsx)(n.td,{children:"Discovers vulnerabilities that are only definable at the specification level"})]}),(0,s.jsxs)(n.tr,{children:[(0,s.jsx)(n.td,{children:(0,s.jsx)(n.strong,{children:"Traceability"})}),(0,s.jsx)(n.td,{children:"Each detection is traceable back to property \u2192 subgraph \u2192 spec section"})]}),(0,s.jsxs)(n.tr,{children:[(0,s.jsx)(n.td,{children:(0,s.jsx)(n.strong,{children:"Comparative analysis"})}),(0,s.jsx)(n.td,{children:"N implementations can be evaluated under the same property vocabulary"})]}),(0,s.jsxs)(n.tr,{children:[(0,s.jsx)(n.td,{children:(0,s.jsx)(n.strong,{children:"FP diagnosis"})}),(0,s.jsx)(n.td,{children:"FPs decompose into three grounded causes (trust boundary / code misreading / spec misunderstanding)"})]})]})]}),"\n",(0,s.jsxs)(n.p,{children:["See ",(0,s.jsx)(n.a,{href:"/en/docs/concepts/proof-attempt",children:"Proof-Attempt Based Auditing"})," for details."]})]})}function h(e={}){let{wrapper:n}={...(0,r.R)(),...e.components};return n?(0,s.jsx)(n,{...e,children:(0,s.jsx)(l,{...e})}):l(e)}},8453(e,n,i){i.d(n,{R:()=>o,x:()=>c});var t=i(6540);let s={},r=t.createContext(s);function o(e){let n=t.useContext(r);return t.useMemo(function(){return"function"==typeof e?e(n):{...n,...e}},[n,e])}function c(e){let n;return n=e.disableParentContext?"function"==typeof e.components?e.components(s):e.components||s:o(e.components),t.createElement(r.Provider,{value:n},e.children)}}}]);
Line numbers count LF bytes from the start of the resource, as the search results do. Vendor segments are library code the classifier recognised; they are stored but not indexed. Bytes are shown as Latin1 characters, one per byte.