arXiv subjects

Sean Noble Anderson

Publications and source records attributed to Sean Noble Anderson.

3 recordsLinked to original sources

arXiv2024

Pipe-Cleaner: Flexible Fuzzing Using Security Policies

Fuzzing has proven to be very effective for discovering certain classes of software flaws, but less effective in helping developers process these discoveries. Conventional crash-based fuzzers lack enough information about failures to determine their root causes, or to differentiate between new or known crashes, forcing developers to manually process long, repetitious lists of crash reports. Also, conventional fuzzers typically cannot be configured to detect the variety of bugs developers care about, many of which are not easily converted into crashes. To address these limitations, we propose Pipe-Cleaner, a system for detecting and analyzing C code vulnerabilities using a refined fuzzing approach. Pipe-Cleaner is based on flexible developer-designed security policies enforced by a tag-based runtime reference monitor, which communicates with a policy-aware fuzzer. Developers are able to customize the types of faults the fuzzer detects and the level of detail in fault reports. Adding more detail helps the fuzzer to differentiate new bugs, discard duplicate bugs, and improve the clarity of results for bug triage. We demonstrate the potential of this approach on several heap-related security vulnerabilities, including classic memory safety violations and two novel non-crashing classes outside the reach of conventional fuzzers: leftover secret disclosure, and heap address leaks.

cs.CR↗

arXiv2024

Foundational Verification of Smart Contracts through Verified Compilation

Programs executed on a blockchain - smart contracts - have high financial stakes; their correctness is crucial. We argue, that this correctness needs to be foundational: correctness needs to be based on the operational semantics of their execution environment. In this work we present a foundational system - the DeepSEA system - targeting the Ethereum blockchain as the largest smart contract platform. The DeepSEA system has a small but sufficiently rich programming language amenable for verification, the DeepSEA language, and a verified DeepSEA compiler. Together they enable true end-to-end verification for smart contracts. We demonstrate usability through two case studies: a realistic contract for Decentralized Finance and contract for crowdfunding.

cs.PL↗

arXiv2024

Formalizing Stack Safety as a Security Property

The term stack safety is used to describe a variety of compiler, run-time, and hardware mechanisms for protecting stack memory. Unlike "the heap," the ISA-level stack does not correspond to a single high-level language concept: different compilers use it in different ways to support procedural and functional abstraction mechanisms from a wide range of languages. This protean nature makes it difficult to nail down what it means to correctly enforce stack safety. We propose a new formal characterization of stack safety using concepts from language-based security. Rather than treating stack safety as a monolithic property, we decompose it into an integrity property and a confidentiality property for each of the caller and the callee, plus a control-flow property: five properties in all. This formulation is motivated by a particular class of enforcement mechanisms, the "lazy" stack safety micro-policies studied by Roessler and DeHon, which permit functions to write into one another's frames but taint the changed locations so that the frame's owner cannot access them. No existing characterization of stack safety captures this style of safety; we capture it here by stating our properties in terms of the observable behavior of the system. Our properties go further than previous formal definitions of stack safety, supporting caller- and callee-saved registers, arguments passed on the stack, and tail-call elimination. We validate the properties by using them to distinguish between correct and incorrect implementations of Roessler and DeHon's micro-policies using property-based random testing. Our test harness successfully identifies several broken variants, including Roessler and DeHon's lazy policy; a repaired version of their policy passes our tests.

cs.PL↗