References:
Separation logic, first developed by O’Hearn and Reynolds, is an extension of Hoare’s logic which addresses reasoning about program that access and mutate data structures.
It includes a “frame rule” which enables more compact proofs and specs of imperative programs than before because of its support for local reasoning, where specification and proofs concentrate on the portion of memory used by a program component, and not the entire global state of the system.
Local reasoning helps with the scalability of proofs done in automatic and semi-automatic verification and program analysis tools.
Separation logic has also been applied to concurrent systems, using the separation conjunction to divide reasoning amongst processes or threads in order to make reasoning more efficient.
Reference:
Local Reasoning about Programs that Alter Data Structures. Peter O’Hearn, John Reynolds, and Hongseok Yang.
[A primer on Separation Logic (and Automatic Program Verification and Analysis)](). Peter W. O’Hearn.
Reasoning about pointers.
Pointer aliasing, arising from several pointers to a given cell. Then an alteration to that cell may affect the values of many syntactically unrelated expressions.
Insights:
We suggest that the source of this mismatch is the global view of state taken in most formalisms for reasoning about pointers. In constrast, programmers reason informally in a local way.
Data structures algorithms typically work by applying local surgeries that rearrange small parts of a data structure, such as rotating a small part of a tree or inserting a node into a list.
Informal reasoning usually concentrate on the effects of these surgeries, without picturing the entire memory of a system.
Assumptions about the local reasoning viewpoint:
To understand how a program works, it should be possible for reasoning and specification to the confined to the cells that the program actually accesses. The value of any other cell will automatically remain unchanged.
Local reasoning is intimately tied to the complexity of specifications. Often, a program works with a circumscribed collection of resources, and it stands to reason that a specification should concentrate on just those resources that a program accesses. For example, a program that inserts an element into a linked list need know only about the cells in that list; there is no need (intuitively) to keep track of all other cells in memory when reasoning about the program.
Pointer Arithmetic model.
The model has two components: the store and the heap.
The store is a finite partial function mapping from variables to integers.
The heap is indexed by a subset Locations of the integers, and is accessed using indirect addressing [E] where [E] is an arithmetic expression.
$Ints \triangleq \{…, -1,0,1,…\}$
$Atoms, Locations \subseteq Ints$
$Variables \triangleq \{x,y,…\}$
The central idea of the approach studied in this paper is of a “spatial conjunction”: P * Q, that asserts that P and Q hold for separate parts of memory. The conjunction provides a way to compose assertion that refer to different areas of memory, while retaining disjointness information for each of the conjuncts.
In general, an assertion $P$ denotes a set of states, and $P*Q$ is true of a state just if its heap/RAM commponent can be split into two parts, one of which satisfies P and the other of which satisfies Q.
If you could revise
the fundmental principles of
computer system design
to improve security...
... what would you change?