sysc.tl

Toward a foundational typed assembly language

by on Nov.19, 2014, under paper notes

Title: Toward a foundational typed assembly language
PDF: http://cpl0.net/~argp/papers/7b0f643010e5537ff02debab6b2fce4b.pdf

A paper from 2002 but a very interesting read; it formally defines a type system for a complete assembly language (TAL). The paper gives typing rules for the instructions and for memory allocation; its advantages are verification and reasoning (for things like heap object reachability) with machine-checked proofs.

An implementation (in OCaml) of TAL for x86 is TALx86; includes a type-checker and an assembler.

Original Twitter link: https://twitter.com/_argp/statuses/524588812731969536

Leave a Comment :, , , , , , , , more...

Time-ordered event traces: a new debugging primitive for concurrency bugs

by on Nov.18, 2014, under paper notes

Title: Time-ordered event traces: a new debugging primitive for concurrency bugs
PDF: http://cpl0.net/~argp/papers/4feb0d2508fcab1061401f6212dde8a2.pdf

A methodology and accompanying pintool for root cause analysis of concurrency bugs; it basically records a runtime trace of function calls and returns, their thread IDs and global timestamps, making clear the order in which they execute.

I really liked that the paper includes five case studies, one of which demonstrates a shortcoming of the approach (a quite common one however).

Original Twitter link: https://twitter.com/_argp/statuses/521674700683223041

Leave a Comment :, , , more...

Interprocedural program analysis

by on Nov.17, 2014, under paper notes

I have been reading/thinking about interprocedural (binary mostly) program analysis lately. There are two ways to do it: a) function summaries produced in advance; b) inlining function bodies and (try to) do whole-program analysis. The problem with a) is (possible) reduced accuracy, and with b) scalability.

Have I missed something? Any pointers to relevant work?

Program analysis Jedi @jvanegue suggested SLAM and Daikon.

Relevant Twitter link: https://twitter.com/_argp/statuses/514491405142863872

Leave a Comment :, more...

A first step towards automated detection of buffer overrun vulnerabilities

by on Nov.12, 2014, under paper notes

Title: A first step towards automated detection of buffer overrun vulnerabilities (BOON)
PDF: http://cpl0.net/~argp/papers/24dcd918253f6a44a43ac6612294397f.pdf

I was looking at BOON lately and it has a nice integrated and reusable range solver to check constraints for integer variables. Much faster and scalable than an SMT solver, although imprecise since it is path insensitive.

See BOON’s implementation for the range solver; specifically files boon-1.0/{newsolver.c, constraint-set.sml}.

Original Twitter link: https://twitter.com/_argp/statuses/512231214153871360

Leave a Comment :, , , more...

Undangle: early detection of dangling pointers in use-after-free and double-free vulnerabilities

by on Nov.11, 2014, under paper notes

Title: Undangle: early detection of dangling pointers in use-after-free and double-free vulnerabilities
PDF: http://cpl0.net/~argp/papers/881dc45d33c7bfea662a0889918999e4.pdf

Uses TEMU to produce an execution/allocations log which is then parsed offline; for each freed heap object the pointers to it are labeled as dangling; taint propagation-like techniques are used to track pointers.

Original Twitter link: https://twitter.com/_argp/statuses/505011997445193728

Leave a Comment :, , , , , , more...

Efficiently detecting all dangling pointer uses in production servers

by on Nov.10, 2014, under paper notes

Title: Efficiently detecting all dangling pointer uses in production servers
PDF: http://cpl0.net/~argp/papers/5f11226846ef1fb1e447ca58fbba6d33.pdf

Runtime detection by placing each allocated object on a new virtual page (like pageheap), but mapping multiple virtual pages to the same physical page avoiding physical memory depletion.

Freed objects cause an mprotect on their page, so possible later uses of the object cause an access violation in turn. Implemented as LLVM IR transformation; tested via C -> IR -> transformations -> IR’ -> C’ -> gcc -O3 :)

Original Twitter link: https://twitter.com/_argp/statuses/499961355097866241

Leave a Comment :, , , more...

Type-based memory allocator hardening notes

by on Nov.07, 2014, under paper notes

Internet Explorer’s new g_hIsolatedHeap mitigation is like a poor man’s type-safe memory reuse implementation. “Poor man’s” since instead of real type-safety, it specifies categories of “dangerous” objects that are placed on the isolated heap. An example full implementation of type-safe memory reuse is Cling, a heap manager that restricts memory reuse to same-type objects.

Of course Firefox’s frame poisoning (since 2010) also implements some type-safe memory reuse ideas.

Btw, the above frame poisoning blog post does not refer to Cling, but a much earlier paper on type-safe memory reuse.

Relevant Twitter link: https://twitter.com/_argp/statuses/498798680863145984

1 Comment :, , more...

Memory leak detection based on memory state transition graph

by on Nov.06, 2014, under paper notes

Title: Memory leak detection based on memory state transition graph
PDF: http://cpl0.net/~argp/papers/9d850ea1ce88e3705bd40b56164a6f40.pdf

Memory state transition graph (MSTG) nodes model heap objects’ states; edges are annotated with path conditions (via symbolic execution); used for function summaries and the leak detection algorithm.

Implementation (just binaries, no source code) available at: http://lcs.ios.ac.cn/~xuzb/melton.html

Relevant Twitter link: https://twitter.com/_argp/statuses/490102227819053056

Leave a Comment :, , more...

Path and context sensitive inter-procedural memory leak detection

by on Nov.05, 2014, under paper notes

Title: Path and context sensitive inter-procedural memory leak detection
PDF: http://cpl0.net/~argp/papers/44a45c88f524da1a62fbf91581d8ede9.pdf

Models heap objects, tracks their state (not pointers to), inter-procedural analysis via
function summaries; solver for path feasibility. Straightforward.

Original Twitter link: https://twitter.com/_argp/statuses/487275885872312320

Leave a Comment :, , more...

A memory model for static analysis of C programs

by on Nov.04, 2014, under paper notes

Title: A memory model for static analysis of C programs
PDF: http://cpl0.net/~argp/papers/44f93d2a09e3d91eca160b387db6cd8c.pdf

Nice read; defines a region-based memory model that can describe C semantics and keep track of lvalue expressions; like a poor man’s alias analysis. Implementation available as part of the clang analyzer.

Original Twitter link: https://twitter.com/_argp/statuses/483678143371550720

Leave a Comment :, , more...

Search

Use the form below to search the blog: