[prover] escape analysis to detect leaks of module-internal references

This is an experimental analysis used in an upcoming paper on robust safety for Move. The high-level idea is that:
- We have an abstract "prover" that can show that invariants hold locally within a module: i.e., if you assume `i` holds in the precondition of every public function of a module, the prover can establish when `i` also holds in the postcondition of the function. The Move Prover is a concrete instantiation of this abstract tool, but other instantiations are possible.
- We have an abstract "encapsulator" that can establish when module-local invariants are also global invariants (i.e., hold in every possible program execution, even when the module in question interacts with untrusted code). The analysis in this PR is a concrete instantiation of this abstract tool, but other instantiations are possible.
- When both the prover and the encapsulator approve a (module, `i`) pair, we can establish that `i` holds globally. If the encapsulator says no, there may be an attack where untrusted code can violate `i`.

The encapsulator implementation is an escape analysis that detects when a procedure "leaks" mutable references that point inside of structs declared in the current module. An attacker can use such a reference to violate local invariants that involve the leaked memory.

The PR implements the analysis + tests and adds several utility functions in move-model useful for running the analysis on benchmarks and collecting stats. It reports nothing in the Diem Framework and flags only the `Option::borrow_mut` code in the Move stdlib. This procedure does indeed leak an internal mutable reference, but the reference cannot be used to violate any invariants of the `Option` module.

Closes: aptos-labs#8807

language/move-model/src/ast.rs

@@ -18,15 +18,16 @@ use crate::{
     exp_rewriter::ExpRewriterFunctions,
     model::{
         EnvDisplay, FieldId, FunId, FunctionVisibility, GlobalEnv, GlobalId, Loc, ModuleId, NodeId,
-        QualifiedInstId, SchemaId, SpecFunId, StructId, TypeParameter, GHOST_MEMORY_PREFIX,
+        QualifiedId, QualifiedInstId, SchemaId, SpecFunId, StructId, TypeParameter,
+        GHOST_MEMORY_PREFIX,
     },
     symbol::{Symbol, SymbolPool},
     ty::{Type, TypeDisplayContext},
 };
 use internment::LocalIntern;
 use itertools::Itertools;
 use once_cell::sync::Lazy;
-use std::{borrow::Borrow, fmt::Debug, hash::Hash, ops::Deref};
+use std::{borrow::Borrow, collections::HashSet, fmt::Debug, hash::Hash, ops::Deref};
 
 // =================================================================================================
 /// # Declarations
@@ -755,6 +756,52 @@ impl ExpData {
         }
         None
     }
+
+    /// Collect struct-related operations
+    pub fn struct_usage(&self, usage: &mut BTreeSet<QualifiedId<StructId>>) {
+        self.visit(&mut |e| {
+            if let ExpData::Call(_, oper, _) = e {
+                use Operation::*;
+                match oper {
+                    Select(mid, sid, ..) | UpdateField(mid, sid, ..) | Pack(mid, sid) => {
+                        usage.insert(mid.qualified(*sid));
+                    }
+                    _ => {}
+                }
+            }
+        });
+    }
+
+    /// Collect field-related operations
+    pub fn field_usage(&self, usage: &mut BTreeSet<(QualifiedId<StructId>, FieldId)>) {
+        self.visit(&mut |e| {
+            if let ExpData::Call(_, oper, _) = e {
+                use Operation::*;
+                match oper {
+                    Select(mid, sid, fid) | UpdateField(mid, sid, fid) => {
+                        usage.insert((mid.qualified(*sid), *fid));
+                    }
+                    _ => {}
+                }
+            }
+        });
+    }
+
+    /// Collect vector-related operations
+    pub fn vector_usage(&self, usage: &mut HashSet<Operation>) {
+        self.visit(&mut |e| {
+            if let ExpData::Call(_, oper, _) = e {
+                use Operation::*;
+                match oper {
+                    Index | Slice | ConcatVec | EmptyVec | SingleVec | UpdateVec | IndexOfVec
+                    | ContainsVec | InRangeVec | RangeVec => {
+                        usage.insert(oper.clone());
+                    }
+                    _ => {}
+                }
+            }
+        });
+    }
 }
 
 struct ExpRewriter<'a> {

language/move-model/src/model.rs

@@ -787,6 +787,11 @@ impl GlobalEnv {
         self.source_files.source_slice(loc.file_id, loc.span)
     }
 
+    /// Return the source file name for `file_id`
+    pub fn get_file(&self, file_id: FileId) -> &OsStr {
+        self.source_files.name(file_id)
+    }
+
     /// Return the source file names.
     pub fn get_source_file_names(&self) -> Vec<String> {
         self.file_name_map
@@ -835,12 +840,21 @@ impl GlobalEnv {
 
     /// Writes accumulated diagnostics of given or higher severity.
     pub fn report_diag<W: WriteColor>(&self, writer: &mut W, severity: Severity) {
+        self.report_diag_with_filter(writer, |d| d.severity >= severity)
+    }
+
+    /// Writes accumulated diagnostics that pass through `filter`
+    pub fn report_diag_with_filter<W: WriteColor, F: Fn(&Diagnostic<FileId>) -> bool>(
+        &self,
+        writer: &mut W,
+        filter: F,
+    ) {
         let mut shown = BTreeSet::new();
         for (diag, reported) in self
             .diags
             .borrow_mut()
             .iter_mut()
-            .filter(|(d, _)| d.severity >= severity)
+            .filter(|(d, _)| filter(d))
         {
             if !*reported {
                 // Avoid showing the same message twice. This can happen e.g. because of
@@ -891,6 +905,14 @@ impl GlobalEnv {
         inv_ids
     }
 
+    pub fn get_global_invariants_for_module(&self, module_id: ModuleId) -> Vec<&GlobalInvariant> {
+        self.global_invariants
+            .iter()
+            .filter(|(_, inv)| inv.declaring_module == module_id)
+            .map(|(_, inv)| inv)
+            .collect()
+    }
+
     pub fn get_global_invariants_by_module(&self, module_id: ModuleId) -> BTreeSet<GlobalId> {
         self.global_invariants
             .iter()
@@ -1431,6 +1453,46 @@ impl GlobalEnv {
             .get(&node_id)
             .and_then(|info| info.instantiation.clone())
     }
+
+    /// Return the total number of declared functions in the modules of `self`
+    pub fn get_declared_function_count(&self) -> usize {
+        let mut total = 0;
+        for m in &self.module_data {
+            total += m.module.function_defs().len();
+        }
+        total
+    }
+
+    /// Return the total number of declared structs in the modules of `self`
+    pub fn get_declared_struct_count(&self) -> usize {
+        let mut total = 0;
+        for m in &self.module_data {
+            total += m.module.struct_defs().len();
+        }
+        total
+    }
+
+    /// Return the total number of Move bytecode instructions (not stackless bytecode) in the modules of `self`
+    pub fn get_move_bytecode_instruction_count(&self) -> usize {
+        let mut total = 0;
+        for m in self.get_modules() {
+            for f in m.get_functions() {
+                total += f.get_bytecode().len();
+            }
+        }
+        total
+    }
+
+    /// Return the total number of Move modules that contain specs
+    pub fn get_modules_with_specs_count(&self) -> usize {
+        let mut total = 0;
+        for m in self.get_modules() {
+            if m.has_specs() {
+                total += 1
+            }
+        }
+        total
+    }
 }
 
 impl Default for GlobalEnv {
@@ -2072,6 +2134,32 @@ impl<'env> ModuleEnv<'env> {
             .disassemble()
             .expect("Failed to disassemble a verified module")
     }
+
+    /// Return true if the module has any global, module, function, or struct specs
+    pub fn has_specs(&self) -> bool {
+        // module specs
+        if self.get_spec().has_conditions() {
+            return true;
+        }
+        // function specs
+        for f in self.get_functions() {
+            if f.get_spec().has_conditions() || !f.get_spec().on_impl.is_empty() {
+                return true;
+            }
+        }
+        // struct specs
+        for s in self.get_structs() {
+            if s.get_spec().has_conditions() {
+                return true;
+            }
+        }
+        // global specs
+        let global_invariants = self.env.get_global_invariants_by_module(self.get_id());
+        if !global_invariants.is_empty() {
+            return true;
+        }
+        false
+    }
 }
 
 // =================================================================================================