Value-range analysis of C programs. Towards proving the absence of buffer overflow vulnerabilities

MaRDI QIDQ3499221zbMATH OpenFDO

Authors Axel Simon

Publication date 28 May 2008

zbMATH Keywords

buffer overflowCcorrectnesspolyhedronsecurity vulnerability

Mathematics Subject Classification ID

Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Static Analysis of String Manipulations in Critical Embedded C Programs
• scientific article; zbMATH DE number 1324833
• Program Analysis Using Symbolic Ranges
• Analyzing string buffers in C
• Interprocedural and flow-sensitive type analysis for memory and type safety of C code

Cited in

(11)

• Exact join detection for convex polyhedra and other numerical abstractions
• Speeding up polyhedral analysis by identifying common constraints
• Analyzing string buffers in C
• Generalizing the template polyhedral domain
• Splitting the Control Flow with Boolean Flags
• Program Analysis Using Symbolic Ranges
• Static Analysis of String Manipulations in Critical Embedded C Programs
• Logahedra: a new weakly relational domain
• Static Analysis
• Canonical forms and widening for two variables per inequality systems
• Interprocedural and flow-sensitive type analysis for memory and type safety of C code

Describes a project that uses

Uses Software

• CSSV
• Octagon

This page was built for publication: Value-range analysis of C programs. Towards proving the absence of buffer overflow vulnerabilities

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3499221)