policies.txt

Tag Policies for Stack Safety Properties
---------------------------------------

This is intended to be a summary from first principles of how we can
enforce the stack safety properties developed in formal.v using PUMP tags
for RISC-V. This requires both defining a micropolicy and specifying
some restrictions on the forms of programs that we expect the micropolicy
to protect.  The style is deliberately tutorial, as I was trying to
re-understand all this myself. I also hope will be helpful as a basis
for writing the relevant part of the paper.

The basic idea of these micropolicies is to associate an integer tag
value (activation-id) with each function activation. During normal
execution the PC tag carries (IN current-activation-id), and this is
used to is used to gate read and store operations (strictly or lazily
depending on the property of interest).  For example, lazy checking
would include this rule:

loadGrp(
       code == {Instr}, env == {IN a}, addr == _, mem == {Stack a} 
    -> env = env, res = {})

restricting loads to values whose tags match the current
activation. Eager checking would also have a rule

storeGrp(
	code == {Instr}, env == {IN a}, addr == _, val == {_}, mem = {Stack a}
    -> 	env = env, mem = {Stack a})

For now, assume that the activation-id is an  unique abstract value  generated
when the activation is first entered. We consider alternatives at
the end of this document. 

Also, assume for now that no arguments are passed on the stack, i.e.
the arg count associated with each call map entry is 0; we'll address
the general case below.

The first fundamental challenge is to make the current activation tag
change at just those points where the property contour changes:

- from caller to callee when the machine executes an instruction
marked as a call point in the call map;

- from callee back to caller when execution reaches the instruction
following the call, with the same sp.

A key characteristic of the contour definitions in our properties is
that the access rights of callers always subsume those of callees.
Hence, while it is essential that the micropolicy changes tags when the
property thinks a call occurs, it is actually safe for the micropolicy to
fail to reset to the caller's tag when the property thinks a return
occurs.  (Dually, it is safe for the micropolicy to change tags even
without executing at a call point, but not for it to reset tags to the
caller when the property thinks execution is still in the caller.)  We
rely heavily on this fact below.

Note: This asymmetry seems rather delicate; it is easy to imagine
properties for which we would need the micropolicy to detect both
calls and returns precisely. This would probably require identifying
return points as well as call points in the property.

The obvious way to handle calls is to require that each call point
instruction tag be marked as a "Call" and to change the PC IN tag to a
fresh activation-id at this point, remembering the caller's
activation-id in the return address:

jalGrp/jalrGrp (
       code = {Instr, Call}, env = {IN caller}
    -> env = {IN new}, return = {RETADDR caller})

To match this, we can tentatively mark jalr instructions to change the
PC tag back provided the target is a return address:

jalrGrp (
	code = {Instr, Return}, target = {RETADDR caller}, env = {_}
    -> 	env = {IN caller}, return = {})

Note that because the property does not identify return sites, we have
no way to require that the "intended" return instructions are tagged
with Return. Some "intended" returns might not be tagged -- which is
OK, as noted above. And some "unintended" jumps might also be so
tagged, but given the property's definition of what a return is, that
is also OK, provided the jump really has the effect of a legal return.

But therein lies the rub: the rules above are much too naive to enforce
the property's idea of returns!

First of all, there is no guarantee that the target contains the
return address for the _current_ activation; it might have been
generated by any previous call at an arbitrary location and level.

Probably the simplest way to fix this is to include both caller and
callee activation-id's in the RETADDR tag:

jalGrp/jalrGrp (
       code = {Instr, Call}, env = {IN caller}
    -> let callee = new in env = {IN callee}, return = {RETADDR caller,IN callee})  
(* NB this "let" is not actually writable in DPL *)

jalrGrp (
	code = {Instr, Return}, target = {RETADDR caller,IN callee}, env = {IN callee}
    -> 	env = {IN caller}, return = {})

But we're not done. Although we now match return addresses correctly,
we are not doing anything to ensure that the stack pointer is reset to
what it was at the call point before changing tags.

To address this problem we turn to a much heavier-weight mechanism:
defining "blessed" entry and exit instruction sequences for functions.
These are specific sequences of tagged instructions that are intended
to appear at the begining and end of each function.   Sequences can
be statically checked for well-formedness, and only programs whose
sequences are well-formed are protected by the micropolicy.  However,
programs remain protected even if the "intended" seqeunces are missing;
the program will simply fail-stop.

Sequences are designed to use instruction tags and PC tag state to
ensure that each sequence is executed in its entirety and in proper
order, and that an entry sequence is executed immediately after each
marked call.  (We could also guarantee that control only passes to the
instruction just after a marked call from an exit sequence.  [There is
an irritating side condition that the caller must not jump to that
location directly, skipping the call.]  With the current property
definitions, there is probably no need to do this, but as noted above,
we can imagine properties for which it would be.)

The details of how to enforce sp behavior depend on how much
flexibility we want to allow in the code.  The simplest thing is
require that each stack frame's size is fixed by adjusting sp at the
beginning of the function, and not changing it thereafter. To cover
this, the (single-instruction) entry sequence simply increments the sp by
n and tags it with a special "saved SP" tag, and the (two-instruction)
exit sequence decrements the sp by n after checking that it has the
special "saved SP" tag, and then does the return.  If any intervening
code overwrites the sp, the exit sequence will fail, which is safe.

In more detail, here is the call:

jal/jalr _   tagged Call

jalGrp/jalrGrp (
     code = {Instr, Call}, env = {IN caller}
  -> let callee = new in env = {IN callee,Entry1}, return = {RETADDR caller,IN callee})  

The entry sequence (singleton):

addi sp,n,sp  tagged Entry1

immArithGrp(
     code == {Instr, Entry1}, env == [+Entry1], op1 == {_}, op2 == {_} 
  -> env = env[-Entry1, res = {SP})

The exit sequence:

addi sp,-n,sp  tagged Exit1   (note: n must be the same as in the entry sequence)
jalr ra        tagged Return

immArithGrp(
     code == {Instr, Exit1}, env == {_}, op1 == {SP}, op2 == {_} 
  -> env = env[-Exit1,+Return], res = {})

jalrGrp (
     code = {Instr, Return}, target = {RETADDR caller,IN callee}, env = {IN callee, Return}
  -> env = {IN caller}, return = {})

Note that control cannot transfer directly to a Return-tagged
instruction because the PC tag only contains Return if we have just
executed the Exit1 instruction.  The same approach can be used to 
avoid jumping into the middle of longer blessed sequences.


Many variations on this basic pattern are possible. A couple of examples:

(i) To allow arbitrary-size frames, we could adopt use of a frame
pointer fp.  The entry sequence stores the old fp on the stack, and
sets the fp to the sp, giving it a special tag.  The exit sequence
resets sp to fp (provided the tag is set on fp), and restores the old
fp (setting the special tag).

(ii) The entry sequence could store the return address on the stack where the exit
sequence retrieves it, avoiding the need for remembering the callee's activation-id
as part of the return address tag.

It turns out that entry and exit sequences are also useful for implementing
other features.  Here are some we need to consider:

EAGER POLICIES AND DEPTH-BASED TAGS:

With unique activation-ids, eager policies work almost exactly like lazy ones; the only difference
is in the store rule.  With depth-based tags, lazy policies clearly fail, because stale tags may
persist after functions return. But eager policies should
still work provided that each frame is initialized during function entry and cleared during function
exit. More specifically, following Nick and Andre's paper:

- Initially the entire stack is marked "No Depth"
- On function entry at depth n, each frame location is marked "Depth n".
- Reads and writes in the function body insist that the memory tag match the current depth.
- On function exit, frame locations are restored to "No Depth."

This can presumably be done as part of the blessed entry and exit sequences, although
the details seem messy.  If we want to pin down exactly what the blessed sequences
are, we have to commit to a code sequence to to the tagging (e.g. via a loop) whereas
in reality a compiler would choose from a variety of code sequences depending on the
number of addresses that need tagging. So instead, we should try to characterize the
_effect_ of the blessed sequences.

[I had some concerns about what it means to get the size of the frame "right"
for the depth-based schemes, but now I cannot see that they are any different from
the unique acivation schemes.]

ARGUMENT PASSING ON THE STACK.

In principle this seems straightforward: the argument values should be written by the caller
using the new activation-id for the callee.  This can be done as part of a "pre-entry" sequence prior to
the call. However, if we are using unique abstract activation-ids there is a technical problem: we
don't get the new id until we perform the call, but we need it several instructions ahead of
time. One solution is to expose the fact that "new" simply bumps an integer counter to predict
what the callee's activation-id will be. But it would be better to avoid this if possible in order
to allow possible GC and re-use of tag values.