Skeleton and initial support for proof-carrying code. (#7165)

* WIP veriwasm 2.0

Co-Authored-By: Chris Fallin <cfallin@fastly.com>

* PCC: successfully parse some simple facts.

Co-authored-by: Nick Fitzgerald <fitzgen@gmail.com>

* PCC: plumb facts through VCode and add framework on LowerBackend to check them.

Co-authored-by: Nick Fitzgerald <fitzgen@gmail.com>

* PCC: code is carrying some proofs! Very simple test-case.

Co-authored-by: Nick Fitzgerald <fitzgen@gmail.com>

* PCC: add a `safe` flag for checked memory accesses.

* PCC: add pretty-printing of facts to CLIF output.

* PCC: misc. cleanups.

* PCC: lots of cleanup.

* Post-rebase fixups and some misc. fixes.

* Add serde traits to facts.

* PCC: add succeed and fail tests.

* Review feedback: rename `safe` memflag to `checked`.

* Review feedback.

---------

Co-authored-by: Nick Fitzgerald <fitzgen@gmail.com>

cranelift/codegen/meta/src/shared/settings.rs

@@ -63,6 +63,15 @@ pub(crate) fn define() -> SettingGroup {
  true,
  );
 
+ settings.add_bool(
+ "enable_pcc",
+ "Enable proof-carrying code translation validation.",
+ r#"
+ This adds a proof-carrying code mode. TODO ADD MORE
+ "#,
+ false,
+ );
+
  // Note that Cranelift doesn't currently need an is_pie flag, because PIE is
  // just PIC where symbols can't be pre-empted, which can be expressed with the
  // `colocated` flag on external functions and global values.

cranelift/codegen/src/context.rs

@@ -237,6 +237,8 @@ impl Context {
  /// Run the verifier on the function.
  ///
  /// Also check that the dominator tree and control flow graph are consistent with the function.
+ ///
+ /// TODO: rename to "CLIF validate" or similar.
  pub fn verify<'a, FOI: Into<FlagsOrIsa<'a>>>(&self, fisa: FOI) -> VerifierResult<()> {
  let mut errors = VerifierErrors::default();
  let _ = verify_context(&self.func, &self.cfg, &self.domtree, fisa, &mut errors);

cranelift/codegen/src/ir/dfg.rs

@@ -5,6 +5,7 @@ use crate::ir;
 use crate::ir::builder::ReplaceBuilder;
 use crate::ir::dynamic_type::{DynamicTypeData, DynamicTypes};
 use crate::ir::instructions::{CallInfo, InstructionData};
+use crate::ir::pcc::Fact;
 use crate::ir::{
  types, Block, BlockCall, ConstantData, ConstantPool, DynamicType, ExtFuncData, FuncRef,
  Immediate, Inst, JumpTables, RelSourceLoc, SigRef, Signature, Type, Value,
@@ -125,6 +126,9 @@ pub struct DataFlowGraph {
  /// Primary value table with entries for all values.
  values: PrimaryMap<Value, ValueDataPacked>,
 
+ /// Facts: proof-carrying-code assertions about values.
+ pub facts: SecondaryMap<Value, Option<Fact>>,
+
  /// Function signature table. These signatures are referenced by indirect call instructions as
  /// well as the external function references.
  pub signatures: PrimaryMap<SigRef, Signature>,
@@ -158,6 +162,7 @@ impl DataFlowGraph {
  dynamic_types: DynamicTypes::new(),
  value_lists: ValueListPool::new(),
  values: PrimaryMap::new(),
+ facts: SecondaryMap::new(),
  signatures: PrimaryMap::new(),
  old_signatures: SecondaryMap::new(),
  ext_funcs: PrimaryMap::new(),

cranelift/codegen/src/ir/memflags.rs

@@ -6,10 +6,19 @@ use core::fmt;
 use serde_derive::{Deserialize, Serialize};
 
 enum FlagBit {
+ /// Guaranteed not to trap. This may enable additional
+ /// optimizations to be performed.
  Notrap,
+ /// Guaranteed to use "natural alignment" for the given type. This
+ /// may enable better instruction selection.
  Aligned,
+ /// A load that reads data in memory that does not change for the
+ /// duration of the function's execution. This may enable
+ /// additional optimizations to be performed.
  Readonly,
+ /// Load multi-byte values from memory in a little-endian format.
  LittleEndian,
+ /// Load multi-byte values from memory in a big-endian format.
  BigEndian,
  /// Accesses only the "heap" part of abstract state. Used for
  /// alias analysis. Mutually exclusive with "table" and "vmctx".
@@ -20,10 +29,15 @@ enum FlagBit {
  /// Accesses only the "vmctx" part of abstract state. Used for
  /// alias analysis. Mutually exclusive with "heap" and "table".
  Vmctx,
+ /// Check this load or store for safety when using the
+ /// proof-carrying-code framework. The address must have a
+ /// `PointsTo` fact attached with a sufficiently large valid range
+ /// for the accessed size.
+ Checked,
 }
 
-const NAMES: [&str; 8] = [
- "notrap", "aligned", "readonly", "little", "big", "heap", "table", "vmctx",
+const NAMES: [&str; 9] = [
+ "notrap", "aligned", "readonly", "little", "big", "heap", "table", "vmctx", "checked",
 ];
 
 /// Endianness of a memory access.
@@ -48,7 +62,7 @@ pub enum Endianness {
 #[derive(Clone, Copy, Debug, Hash, PartialEq, Eq)]
 #[cfg_attr(feature = "enable-serde", derive(Serialize, Deserialize))]
 pub struct MemFlags {
- bits: u8,
+ bits: u16,
 }
 
 impl MemFlags {
@@ -265,6 +279,32 @@ impl MemFlags {
  self.set_vmctx();
  self
  }
+
+ /// Test if the `checked` bit is set.
+ ///
+ /// Loads and stores with this flag are verified to access
+ /// pointers only with a validated `PointsTo` fact attached, and
+ /// with that fact validated, when using the proof-carrying-code
+ /// framework. If initial facts on program inputs are correct
+ /// (i.e., correctly denote the shape and types of data structures
+ /// in memory), and if PCC validates the compiled output, then all
+ /// `checked`-marked memory accesses are guaranteed (up to the
+ /// checker's correctness) to access valid memory. This can be
+ /// used to ensure memory safety and sandboxing.
+ pub fn checked(self) -> bool {
+ self.read(FlagBit::Checked)
+ }
+
+ /// Set the `checked` bit.
+ pub fn set_checked(&mut self) {
+ self.set(FlagBit::Checked);
+ }
+
+ /// Set the `checked` bit, returning new flags.
+ pub fn with_checked(mut self) -> Self {
+ self.set_checked();
+ self
+ }
 }
 
 impl fmt::Display for MemFlags {

cranelift/codegen/src/ir/mod.rs

@@ -18,6 +18,7 @@ pub(crate) mod known_symbol;
 pub mod layout;
 pub(crate) mod libcall;
 mod memflags;
+pub mod pcc;
 mod progpoint;
 mod sourceloc;
 pub mod stackslot;