Backtranslation

[dongjaelee1]

Compiles except for security/Blame.v, security/Recomposition.v.

This PR is not ready for merge.

Theorem backtranslation_proof in security/BacktranslationProof2.v proves that there exists a Clight program which can generate a trace with the same prefix as generated from an original (whole) Asm program:

  Hypothesis EFO: external_functions_observable.
  Hypothesis IAO: inline_assembly_observable.

  Theorem backtranslation_proof
          (p: Asm.program)
          (WF: asm_program_is_wf p)
    :
    forall tr,
      (Z.of_nat (length tr) < Int64.modulus) ->
      asm_program_does_prefix p tr ->
      exists p_c,
        clight_program_does_prefix p_c tr.

Assumptions

1. The theorem assumes some reasonable well-formedness conditions on the original assembly program as expressed by asm_program_is_wf.

This says that the Asm program should

• not have multiple definitions for the same identifier
• the public identifiers should have definitions
• the main should be defined, and it should be an internal function with the correct signature (signature_main)
• memory initialization should success (exists an initial memory)

2. It also assumes that any external functions or inline assembly (parameters in CompCert) should generate at least one event (in other words, they should not generate an empty event).

This condition is essential for the counter-based backtranslation to work in the presence of CompCert-style external call semantics.
CompCert has relational-style semantics for user-given external calls, and for a program to process an external call, it needs some other witness of the same external call (which is usually not a problem in a simulation proof).

However, this implies that backtranslation must generate the same external calls to correctly follow the execution of the original Asm program.
The is a problematic for the counter-based backtranslation when the external call is silent.
Consider the following (pseudo-assembly) code:

L1: some_external_call
L2: goto L1

If some_external_call does not generate any event, this code exhibits a silent divergence, where the trace has length 0.
However, backtranslation still needs to generate a code which repeatedly calls some_external_call.
This means that the counter used by the backtranslated program can blow up, exceeding the length of the original trace.
This second assumption resolves this issue by ensuring that the user-given external calls to generate at least one event.

Notes

1. The Asm semantics is slightly changed to step_fix.

Fixing the semantics and the compiler-correctness proofs should not be difficult.
Also, I am not aware of the most up-to-date Asm semantics, so someone should resolve conflicts.

Jérémy is aware of this issue, and I believe he can handle this.

2. Some changes in the external call semantics. They can be found in common/Events.v

2-1. The following axiom is added to extcall_properties:

(** External calls cannot free public blocks without the Max Freeable permission *)
  ec_public_not_freeable:
    forall ge vargs m1 t vres m2 b ofs id,
    sem ge vargs m1 t vres m2 ->
    Mem.valid_block m1 b ->
    Senv.invert_symbol ge b = Some id -> Senv.public_symbol ge id = true ->
    Mem.perm m1 b ofs Max Nonempty -> (~ Mem.perm m1 b ofs Max Freeable) ->
    Mem.perm m2 b ofs Max Nonempty;

This have been discussed before, and proofs are fixed accordingly.

2-2. EF_memcpy: the destination pointer should not be a block for a public symbol (EF_memcpy_dest_not_pub).

This change is mostly to reduce proof complexity.
Current proof assumes that any memory store is done by Mem.storev, but memcpy uses Mem.storebyes, becoming the only exception.
Removing this will require nontrivial extensions in current proof.

2-3. EF_vstore: the stored value v should be whole against the memory chunk ch (Val.load_result ch v = v), which usually means that the chunk size is 32/64 bit, or sign/zero-extension does not modify the value (EF_vstore_load_whole_chunk).

This change is needed to correctly generate C-level types.
In C-level, there can be multiple definitions of EF_vstore with different argument types, each reflecting the different chunk sizes.
This information is used in the Clight semantics when calling EF_vstore.
For instance, if EF_vstore is storing a signed 8-bit sized int, the global environment must have a EF_vstore with Tint 8-bit signed type.

However, those argument types are erased in the assembly level, and correctly backtranslating each definition of EF_vstore will also require nontrivial extensions in current proof.