Why Smart Contracts Fail: Undiscovered bugs and what we can do about them – Medium edit / delete

Turns out that if you build a digital cash system where people can write code to specify behaviour, then that code has bugs in it. Who'd have thought it?

to blockchain bugs ethereum security static-analysis ... on 28 August 2016

Security/Projects/Bandit - OpenStack edit / delete

A security scanner for Python code.

to python security static-analysis ... on 23 March 2015

Axiomatic validation of memory barriers and atomic instructions [LWN.net] edit / delete

More progress on model checking for memory models on modern processors. The tool described here covers ARM, Power and x86 memory models, and does efficient analysis of (smallish) chunks of code.

to arm atomic concurrency herd intel memory memory-model model-checking power static-analysis x86 ... on 28 August 2014

How to Prevent the next Heartbleed edit / delete

An interesting review of some of the approaches that didn't prevent the OpenSSL heartbeat bug (either because they weren't effective or because they weren't applied).

to buffer-overflow checking openssl security static-analysis testing ... on 02 May 2014

Embedded in Academia : A New Development for Coverity and Heartbleed edit / delete

What Coverity is doing to detect the Heartbleed problem (in short: treating n2hs-style functions as generating tainted results).

to coverity security ssl static-analysis tls ... on 14 April 2014

The Power of Ten -- Rules for Writing Safety Critical Code edit / delete

This largely matches what I'd recommend anyway, but perhaps I should encourage students to make more use of assertions. This could be summarised as "make it possible to do static analysis on your code".

to ag0700 c coding-style safety static-analysis ... on 26 March 2014

checkedthreads: bug-free shared memory parallelism edit / delete

Fork-join framework with static checking assisted by Valgrind. Good description of how the analysis works.

to ag0803 concurrency parallel software static-analysis valgrind ... on 15 December 2013

Frama-C edit / delete

to c software static-analysis ... on 24 March 2012

Eliminating Array Bound Checking through Non-dependent types edit / delete

A neat trick: using existentially-qualified (but unspecified) types to track instances of arrays at the type level.

to haskell research static-analysis typechecking ... on 18 August 2008

Browser bookmarks: tasty+ | tasty= Log in | Export | Atom