Repository: project-oak/oak
Pull request #1699 (2020-11-05 22:16:37)

Low projection makes labels themselves partially secret
The commit messages are worth reading as a guide for the most significant changes,

particularly the commit message for "[WIP]Working on unobs; need significant def change"

The proof state is roughly where it was before despite the low-level definitional change.

I fixed and then unfixed the spacing in NIUtils to make the PR readable temporarily :) 

# Checklist

- [ ] Pull request affects core Oak functionality (e.g. runtime, SDK, ABI)
  - [ ] I have written tests that cover the code changes.
  - [ ] I have checked that these tests are run by
        [Cloudbuild](/cloudbuild.yaml)
  - [ ] I have updated [documentation](/docs/) accordingly.
  - [ ] I have raised an [issue](https://github.com/project-oak/oak/issues) to
        cover any TODOs and/or unfinished work.
- [ ] Pull request includes prototype/experimental work that is under
      construction.



Patch:
diff --git a/docs/programming-oak.md b/docs/programming-oak.md
index f84df726a2..fd465eac5c 100644
--- a/docs/programming-oak.md
+++ b/docs/programming-oak.md
@@ -64,7 +64,7 @@ oak::entrypoint!(grpc_oak_main<ConfigMap> => |_receiver| {
     };
     let grpc_channel =
         oak::grpc::server::init("[::]:8080").expect("could not create gRPC server pseudo-Node");
-    oak::run_command_loop(node, grpc_channel.iter());
+    oak::run_command_loop(MachineLearningDispatcher::new(node), grpc_channel.iter());
 });
 ```
 <!-- prettier-ignore-end -->
@@ -579,7 +579,7 @@ async fn test_say_hello() {
     let runtime = oak_tests::run_single_module_default(MODULE_WASM_FILE_NAME)
         .expect("Unable to configure runtime with test wasm!");
 
-    let (channel, interceptor) = oak_tests::channel_and_interceptor().await;
+    let (channel, interceptor) = oak_tests::public_channel_and_interceptor().await;
     let mut client = HelloWorldClient::with_interceptor(channel, interceptor);
 
     let req = HelloRequest {
diff --git a/examples/Cargo.lock b/examples/Cargo.lock
index 220491ee72..783caaa4dd 100644
--- a/examples/Cargo.lock
+++ b/examples/Cargo.lock
@@ -912,6 +912,7 @@ dependencies = [
  "oak",
  "oak_abi",
  "oak_io",
+ "oak_utils",
  "prost",
  "rand 0.7.3",
  "rand_distr",
@@ -1157,6 +1158,7 @@ version = "0.1.0"
 dependencies = [
  "either",
  "hex",
+ "log",
  "oak_abi",
  "oak_derive",
  "oak_utils",
diff --git a/examples/machine_learning/module/rust/Cargo.toml b/examples/machine_learning/module/rust/Cargo.toml
index 889d38047d..ba33c2a6fc 100644
--- a/examples/machine_learning/module/rust/Cargo.toml
+++ b/examples/machine_learning/module/rust/Cargo.toml
@@ -17,3 +17,6 @@ oak_abi = "=0.1.0"
 oak_io = "=0.1.0"
 log = "*"
 prost = "*"
+
+[build-dependencies]
+oak_utils = "*"
diff --git a/examples/machine_learning/module/rust/build.rs b/examples/machine_learning/module/rust/build.rs
new file mode 100644
index 0000000000..9b4ee9a02e
--- /dev/null
+++ b/examples/machine_learning/module/rust/build.rs
@@ -0,0 +1,22 @@
+//
+// Copyright 2019 The Project Oak Authors
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+//
+
+fn main() {
+    oak_utils::compile_protos(
+        &["../../proto/machine_learning.proto"],
+        &["../../proto", "../../../../third_party"],
+    );
+}
diff --git a/examples/machine_learning/module/rust/src/lib.rs b/examples/machine_learning/module/rust/src/lib.rs
index 1d719facaa..cac8ceb3f7 100644
--- a/examples/machine_learning/module/rust/src/lib.rs
+++ b/examples/machine_learning/module/rust/src/lib.rs
@@ -17,12 +17,20 @@
 // This model was inspired by
 // https://github.com/AtheMathmo/rusty-machine/blob/master/examples/naive_bayes_dogs.rs .
 
-use log::{error, info, warn};
+pub mod proto {
+    include!(concat!(
+        env!("OUT_DIR"),
+        "/oak.examples.machine_learning.rs"
+    ));
+}
+
+use log::{info, warn};
 use oak::{
     grpc,
     io::{Receiver, ReceiverExt},
 };
 use oak_abi::proto::oak::application::ConfigMap;
+use proto::{MachineLearning, MachineLearningDispatcher, MlData, MlLearn, MlPredict, MlResponse};
 use rand::prelude::*;
 use rand_distr::{Distribution, Normal, Standard};
 use rusty_machine::{
@@ -158,7 +166,7 @@ oak::entrypoint!(oak_main<grpc::Invocation> => |receiver: Receiver<grpc::Invocat
         config: None,
         model: NaiveBayes::new(),
     };
-    oak::run_command_loop(node, receiver.iter());
+    oak::run_command_loop(MachineLearningDispatcher::new(node), receiver.iter());
 });
 
 oak::entrypoint!(grpc_oak_main<ConfigMap> => |_receiver| {
@@ -171,7 +179,7 @@ oak::entrypoint!(grpc_oak_main<ConfigMap> => |_receiver| {
     };
     let grpc_channel =
         oak::grpc::server::init("[::]:8080").expect("could not create gRPC server pseudo-Node");
-    oak::run_command_loop(node, grpc_channel.iter());
+    oak::run_command_loop(MachineLearningDispatcher::new(node), grpc_channel.iter());
 });
 
 struct Node {
@@ -181,107 +189,102 @@ struct Node {
     model: NaiveBayes<naive_bayes::Gaussian>,
 }
 
-impl oak::grpc::ServerNode for Node {
-    fn invoke(&mut self, method: &str, _req: &[u8], writer: grpc::ChannelResponseWriter) {
-        match method {
-            "/oak.examples.machine_learning.MachineLearning/Data" => {
-                info!("Data");
-                //(self.training_set_size, self.test_set_size) = (1000, 1000);
-                // Generate all of our train and test data
-                let (training_matrix, target_matrix, test_matrix, test_animals) =
-                    generate_animal_data(self.training_set_size, self.test_set_size);
-                self.config = Some(Config {
-                    training_matrix,
-                    target_matrix,
-                    test_matrix,
-                    test_animals,
-                });
+impl MachineLearning for Node {
+    fn data(&mut self, _req: MlData) -> grpc::Result<MlResponse> {
+        info!("Data");
+        //(self.training_set_size, self.test_set_size) = (1000, 1000);
+        // Generate all of our train and test data
+        let (training_matrix, target_matrix, test_matrix, test_animals) =
+            generate_animal_data(self.training_set_size, self.test_set_size);
+        self.config = Some(Config {
+            training_matrix,
+            target_matrix,
+            test_matrix,
+            test_animals,
+        });
+        Ok(MlResponse::default())
+    }
+    fn learn(&mut self, _req: MlLearn) -> grpc::Result<MlResponse> {
+        info!("Training model");
+        //self.model = NaiveBayes::<naive_bayes::Gaussian>::new();
+        match self.config {
+            Some(ref c) => self
+                .model
+                .train(&c.training_matrix, &c.target_matrix)
+                .expect("failed to train model of dogs"),
+            None => {
+                warn!("config not set");
             }
-            "/oak.examples.machine_learning.MachineLearning/Learn" => {
-                info!("Training model");
-                //self.model = NaiveBayes::<naive_bayes::Gaussian>::new();
-                match self.config {
-                    Some(ref c) => self
-                        .model
-                        .train(&c.training_matrix, &c.target_matrix)
-                        .expect("failed to train model of dogs"),
-                    None => {
-                        warn!("config not set");
-                    }
-                }
+        }
+        Ok(MlResponse::default())
+    }
+    fn predict(&mut self, _req: MlPredict) -> grpc::Result<MlResponse> {
+        info!("Predicting");
+        let mut predictions = None;
+        match self.config {
+            Some(ref c) => {
+                predictions = Some(
+                    self.model
+                        .predict(&c.test_matrix)
+                        .expect("failed to predict dogs!?"),
+                )
             }
-            "/oak.examples.machine_learning.MachineLearning/Predict" => {
-                info!("Predicting");
-                let mut predictions = None;
-                match self.config {
-                    Some(ref c) => {
-                        predictions = Some(
-                            self.model
-                                .predict(&c.test_matrix)
-                                .expect("failed to predict dogs!?"),
-                        )
-                    }
-                    None => {
-                        warn!("config not set");
-                    }
-                }
-                // Score how well we did.
-                let mut hits = 0;
-                let unprinted_total = self.test_set_size.saturating_sub(10) as usize;
-                match self.config {
-                    Some(ref c) => {
-                        if let Some(ref p) = predictions {
-                            for (animal, prediction) in c
-                                .test_animals
-                                .iter()
-                                .zip(p.iter_rows())
-                                .take(unprinted_total)
-                            {
-                                evaluate_prediction(&mut hits, animal, prediction);
-                            }
-                        }
-                    }
-                    None => {
-                        warn!("test_animals not set");
-                        return;
+            None => {
+                warn!("config not set");
+            }
+        }
+        // Score how well we did.
+        let mut hits = 0;
+        let unprinted_total = self.test_set_size.saturating_sub(10) as usize;
+        match self.config {
+            Some(ref c) => {
+                if let Some(ref p) = predictions {
+                    for (animal, prediction) in c
+                        .test_animals
+                        .iter()
+                        .zip(p.iter_rows())
+                        .take(unprinted_total)
+                    {
+                        evaluate_prediction(&mut hits, animal, prediction);
                     }
                 }
+            }
+            None => {
+                warn!("test_animals not set");
+                return Err(grpc::build_status(
+                    grpc::Code::InvalidArgument,
+                    "test_animals not set",
+                ));
+            }
+        }
 
-                if unprinted_total > 0 {
-                    info!("...");
-                }
+        if unprinted_total > 0 {
+            info!("...");
+        }
 
-                if let Some(ref c) = self.config {
-                    if let Some(ref p) = predictions {
-                        for (animal, prediction) in c
-                            .test_animals
-                            .iter()
-                            .zip(p.iter_rows())
-                            .skip(unprinted_total)
-                        {
-                            let (actual_type, accurate) =
-                                evaluate_prediction(&mut hits, animal, prediction);
-                            info!(
-                                "Predicted: {:?}; Actual: {:?}; Accurate? {:?}",
-                                animal.type_, actual_type, accurate
-                            );
-                        }
-                    }
+        if let Some(ref c) = self.config {
+            if let Some(ref p) = predictions {
+                for (animal, prediction) in c
+                    .test_animals
+                    .iter()
+                    .zip(p.iter_rows())
+                    .skip(unprinted_total)
+                {
+                    let (actual_type, accurate) =
+                        evaluate_prediction(&mut hits, animal, prediction);
+                    info!(
+                        "Predicted: {:?}; Actual: {:?}; Accurate? {:?}",
+                        animal.type_, actual_type, accurate
+                    );
                 }
-                info!(
-                    "Accuracy: {}/{} = {:.1}%",
-                    hits,
-                    self.test_set_size,
-                    (f64::from(hits)) / (f64::from(self.test_set_size as u32)) * 100.
-                );
-            }
-            _ => {
-                error!("unknown method name: {}", method);
-                panic!("unknown method name");
             }
         }
-        writer
-            .write_empty(grpc::WriteMode::Close)
-            .expect("Failed to write empty response");
+        info!(
+            "Accuracy: {}/{} = {:.1}%",
+            hits,
+            self.test_set_size,
+            (f64::from(hits)) / (f64::from(self.test_set_size as u32)) * 100.
+        );
+        Ok(MlResponse::default())
     }
 }
diff --git a/experimental/Cargo.lock b/experimental/Cargo.lock
index a43c2d467c..2420b3a9c9 100644
--- a/experimental/Cargo.lock
+++ b/experimental/Cargo.lock
@@ -835,6 +835,7 @@ version = "0.1.0"
 dependencies = [
  "either",
  "hex",
+ "log",
  "oak_abi",
  "oak_derive",
  "oak_utils",
diff --git a/experimental/benchmark/src/application/oak.rs b/experimental/benchmark/src/application/oak.rs
index 93095d1300..d38f9ccfc0 100644
--- a/experimental/benchmark/src/application/oak.rs
+++ b/experimental/benchmark/src/application/oak.rs
@@ -60,7 +60,7 @@ impl OakApplication {
         let runtime = oak_runtime::configure_and_run(config)
             .expect("Couldn't configure runtime with test wasm");
 
-        let (channel, interceptor) = oak_tests::channel_and_interceptor().await;
+        let (channel, interceptor) = oak_tests::public_channel_and_interceptor().await;
         let client = TrustedDatabaseClient::with_interceptor(channel, interceptor);
 
         OakApplication { runtime, client }
diff --git a/experimental/ni_coq/vfiles/LowEquivalences.v b/experimental/ni_coq/vfiles/LowEquivalences.v
index 788f0187a7..eef000e2db 100644
--- a/experimental/ni_coq/vfiles/LowEquivalences.v
+++ b/experimental/ni_coq/vfiles/LowEquivalences.v
@@ -40,8 +40,35 @@ Definition low_proj {A: Type} ell ( labeled_thing: @labeled A) :=
     match labeled_thing with
         | Labeled _ o ell' => if( ell' <<? ell ) 
             then labeled_thing
-            else Labeled A None ell'
+            else Labeled A None top
     end.
+    (* 
+    Importantly, the label of the secret thing is NOT ell'
+    but instead the top of the information flow lattice 
+    (secret, untrusted) which means that in this formulation,
+    labels are not completely public. Instead, an observer at level
+    ell can see:
+        - whether the label of an object flows to ell, for any object.
+        - the precise label of the object if its label does flow to ell.
+    Putting it another way, the label ell' of a secret object is not observable,
+    but whether or not (ell' <<L ell) is observable.
+
+    This defintion is necessary in order to make the theorem provable while
+    still supporting dynamic creation of nodes and channels. 
+    Noninterference proofs often rely on theorems that roughly say "when a
+    secret step is taken, no public state is updated". (In this code, these
+    theorems often have "unobs" in their names. In the literature these are
+    sometimes called clearance). To create a node
+    or channel, a new labeled object appears, which is effectively a "label
+    change". If labels are public, we can't prove the "unobs" theorems because
+    because the node/channel creation calls DO create new labels and therefore
+    do update public state. 
+    
+    By revealing only partial information about labels to an arbitrary
+    observer, we can show that since secret nodes can only create secret
+    objects, these label changes in the secret part of the lattice are actually
+    hidden.
+    *)
 
 Definition node_low_proj := @low_proj node.
 Definition chan_low_proj := @low_proj channel.
diff --git a/experimental/ni_coq/vfiles/NIUtilTheorems.v b/experimental/ni_coq/vfiles/NIUtilTheorems.v
index ca3f8c540c..04310fcd31 100644
--- a/experimental/ni_coq/vfiles/NIUtilTheorems.v
+++ b/experimental/ni_coq/vfiles/NIUtilTheorems.v
@@ -5,7 +5,8 @@ From OakIFC Require Import
         RuntimeModel
         EvAugSemantics
         Events
-        LowEquivalences.
+        LowEquivalences
+        Tactics.
 Require Import Coq.Lists.List.
 Import ListNotations.
 From RecordUpdate Require Import RecordSet.
@@ -32,9 +33,9 @@ Theorem can_split_chan_index: forall s han ch ell,
     (obj (chans s).[? han] = Some ch) /\
     (lbl (chans s).[? han] = ell).
 Proof.
-    intros. split; destruct ((chans s).[? han]).
-    - unfold RuntimeModel.obj. inversion H. reflexivity.
-    - unfold RuntimeModel.lbl. inversion H. reflexivity.
+  intros. split; destruct ((chans s).[? han]).
+  - unfold RuntimeModel.obj. inversion H. reflexivity.
+  - unfold RuntimeModel.lbl. inversion H. reflexivity.
 Qed.
 
 End misc.
@@ -51,7 +52,7 @@ Qed.
 
 Theorem nflows_labeled_proj {A: Type}: forall ell (x: @labeled A),
     ~(lbl x <<L ell) ->
-    (low_proj ell x) = Labeled A None (lbl x).
+    (low_proj ell x) = Labeled A None top.
 Proof.
     intros. destruct x. unfold low_proj. simpl in H.
     destruct (lbl <<? ell); eauto; try contradiction.
@@ -63,10 +64,10 @@ Theorem labeled_low_proj_idempotent {A: Type}:
     forall ell, idempotent (@low_proj A ell).
 Proof.
     intros. unfold idempotent. intros x.
-    destruct x. unfold low_proj. destruct (lbl <<? ell)  eqn:Hflows;
-    rewrite Hflows; eauto.
+    destruct x. unfold low_proj. destruct (lbl <<? ell)  eqn:Hflows.
+    rewrite Hflows; eauto. destruct (top <<? ell); reflexivity.
 Qed.
-
+  
 Definition node_low_proj_idempotent := @labeled_low_proj_idempotent node.
 Definition chan_low_proj_idempotent := @labeled_low_proj_idempotent channel.
 Definition event_low_proj_idempotent := @labeled_low_proj_idempotent event.
@@ -83,8 +84,9 @@ Theorem labeled_low_proj_loweq {A: Type}:
     @low_proj_loweq (@labeled A) low_proj low_eq.
 Proof.
     unfold low_proj_loweq. unfold low_eq. unfold low_proj. intros.
-    destruct x. destruct (lbl <<? ell) eqn:Hflows;
-    rewrite Hflows; reflexivity.
+    destruct x. destruct (lbl <<? ell) eqn:Hflows.
+    rewrite Hflows. reflexivity.
+    destruct (top <<? ell); reflexivity.
 Qed.
 
 Definition node_low_proj_loweq := @labeled_low_proj_loweq node.
@@ -96,17 +98,25 @@ Theorem state_low_proj_loweq:
 Proof.
 Admitted.
 
-Theorem low_projection_preserves_lbl {A: Type}: forall ell (x: @labeled A),
-    (low_proj ell x).(lbl) = x.(lbl).
-Proof.
-    intros. destruct x. simpl. destruct (lbl <<? ell); auto.
+Theorem proj_labels_increase {A: Type }: forall ell ell' (x: @labeled A),
+  ell' <<L x.(lbl) -> ell' <<L (low_proj ell x).(lbl).
+  destruct x. cbv [RuntimeModel.lbl]. unfold low_proj. destruct_match.
+  intros. eauto. intros. eapply top_is_top.
 Qed.
 
-Definition node_projection_preserves_lbl :=
-    @low_projection_preserves_lbl node.
-Definition chan_projection_preserves_lbl := 
-    @low_projection_preserves_lbl channel.
-
+Theorem low_proj_preserves_obs {A: Type}: forall ell (x: @labeled A),
+  x.(lbl) <<L ell <-> (low_proj ell x).(lbl) <<L ell.
+Proof.
+    destruct x. cbv [RuntimeModel.lbl].
+    unfold low_proj. split; destruct_match. 
+    (* -> *)
+    eauto. contradiction.
+    (* <- *)
+    eauto. intros. pose proof (top_is_top ell).
+    replace ell with top by (apply ord_anti; auto).
+    apply top_is_top. 
+Qed.
+    
 Theorem uncons_proj_chan_s: forall ell s han ch,
     (chans (state_low_proj ell s)).[? han] = ch ->
     exists ch',
@@ -162,11 +172,17 @@ Theorem proj_node_state_to_proj_n: forall ell s id nl n,
 Proof.
 Admitted.
 
-Theorem node_projection_preserves_flowsto: forall ell s id n n',
-    s.(nodes).[? id] = n ->
-    (state_low_proj ell s).(nodes).[? id] = n' ->
-    ~(n.(lbl) <<L ell) ->
-    ~(n'.(lbl) <<L ell).
+Theorem proj_preserves_fresh_han: forall ell s h,
+    fresh_han s h ->
+    fresh_han (state_low_proj ell s) h.
+Proof.
+    (* depends on concurrent change to def of states, but
+    should be true *)
+Admitted.
+
+Theorem proj_preserves_fresh_nid: forall ell s id,
+    fresh_nid s id ->
+    fresh_nid (state_low_proj ell s) id.
 Proof.
 Admitted.
 
@@ -174,7 +190,6 @@ End low_projection.
 
 Section low_equivalence.
 
-
 Global Instance node_state_low_eq_refl: forall ell, Reflexive (node_state_low_eq ell) | 10.
 Proof. congruence. Qed.
 
@@ -230,17 +245,6 @@ Proof.
     intros. inversion H0. unfold node_state_low_proj in *. 
 Admitted. 
 
-Theorem node_low_eq_to_lbl_eq: forall ell n1 n2,
-    (node_low_eq ell n1 n2) ->
-    (n1.(lbl) = n2.(lbl)).
-Proof.
-    intros. inversion H.
-    assert ( lbl (low_proj ell n1) = lbl (low_proj ell n2)).
-    rewrite H1. reflexivity.
-    rewrite !node_projection_preserves_lbl in H0.
-    assumption.
-Qed.
-
 Theorem trace_leq_imples_head_st_leq: forall ell t1 t2 s1 s2,
     (head_st t1 = Some s1) ->
     (head_st t2 = Some s2) ->
@@ -271,25 +275,28 @@ Section unobservable.
     not visible to ell the old and new state are ell-equivalent
 *)
 
-Theorem set_call_unobs: forall ell s id n c,
-    (nodes s).[? id] = n ->
-    ~(lbl n <<L ell) ->
+Theorem set_call_unobs: forall ell s id c,
+    ~(lbl (nodes s).[? id] <<L ell) ->
     (state_low_eq ell s (s_set_call s id c)).
 Proof.
 Admitted.
 
-Theorem state_upd_chan_unobs: forall ell s han ch ch',
-    (chans s).[? han] = ch ->
-    ~(lbl ch <<L ell) ->
-    (state_low_eq ell s (state_upd_chan han ch' s)).
+Theorem state_upd_chan_unobs: forall ell s han ch,
+    ~(lbl (chans s).[? han] <<L ell) ->
+    (state_low_eq ell s (state_upd_chan han ch s)).
 Proof.
 Admitted.
 
-Theorem state_upd_node_unobs: forall ell s id n n',
-    (nodes s).[? id] = n ->
-    ~(lbl n <<L ell) ->
-    (state_low_eq ell s (state_upd_node id n' s)).
+Theorem state_chan_append_labeled_unobs: forall ell s han msg,
+    ~(lbl (chans s).[? han] <<L ell) ->
+    (state_low_eq ell s (state_chan_append_labeled han msg s)).
 Proof.
 Admitted.
 
+Theorem state_upd_node_unobs: forall ell s id n,
+    ~(lbl (nodes s).[? id] <<L ell) ->
+    (state_low_eq ell s (state_upd_node id n s)).
+Proof.
+Admitted.
+  
 End unobservable.
diff --git a/experimental/ni_coq/vfiles/PossibilisticNI.v b/experimental/ni_coq/vfiles/PossibilisticNI.v
index 56e7b3831d..94ab54267a 100644
--- a/experimental/ni_coq/vfiles/PossibilisticNI.v
+++ b/experimental/ni_coq/vfiles/PossibilisticNI.v
@@ -120,6 +120,34 @@ Local Ltac apply_all_constructors :=
   | _ => idtac (* ignore goals that don't match one of the previous patterns *)
   end.
 
+Lemma separate_lableled {A} (o : option A) (l : level) (x : labeled) :
+  obj x = o -> lbl x = l -> x = Labeled _ o l.
+Proof. destruct x; cbn; congruence. Qed.
+
+Ltac separate_hyp T :=
+  repeat match goal with
+         | H : ?s = Labeled T ?o ?l |- _ =>
+           assert (obj s = o /\ lbl s = l) by (rewrite H; tauto);
+           clear H; logical_simplify
+         end.
+Ltac separate_goal := apply separate_lableled.
+
+Lemma invert_chans_state_low_proj_flowsto ell lvl s han :
+  lvl <<L ell ->
+  lvl <<L (chans (state_low_proj ell s)).[? han].(lbl) ->
+  lvl <<L (chans s).[? han].(lbl).
+Proof.
+  destruct s.
+  repeat match goal with
+         | _ => progress cbn [state_low_proj
+                               RuntimeModel.chans RuntimeModel.lbl ]
+         | _ => progress cbv [low_proj chan_state_low_proj fnd]
+         | _ => destruct_match
+         | _ => tauto
+         end.
+    intros.
+Admitted.
+
 Hint Resolve multi_system_ev_refl multi_system_ev_tran : multi.
 
 (* Hints for [eauto with unwind] *)
@@ -136,8 +164,11 @@ Hint Extern 4 (state_low_eq _ _ (state_low_proj _ _)) => symmetry : unwind.
 Hint Extern 2 (chan_low_proj _ _ = chan_low_proj _ _)
 => simple eapply chan_low_proj_loweq : unwind.
 
-Hint Extern 4 (_ <<L lbl (chan_low_proj _ _))
-=> (rewrite chan_projection_preserves_lbl) : flowsto.
+(* hits for eauto in event part of the unobservable step proof *)
+Hint Extern 4 (low_proj _ _  = _ ) => erewrite nflows_labeled_proj : unobs_ev.
+Hint Extern 4 (_  = low_proj _ _ ) => erewrite nflows_labeled_proj : unobs_ev.
+Hint Extern 4 (event_low_eq _ _ _) => unfold event_low_eq : unobs_ev.
+Hint Extern 4 (low_eq _ _ _) => unfold low_eq : unobs_ev.
 
 Definition is_init(t: trace) := length t = 1.
 
@@ -152,6 +183,47 @@ Definition conjecture_possibilistic_ni := forall ell t1_init t2_init t1n,
         (step_system_ev_multi t2_init t2n) /\
         (trace_low_eq ell t1n t2n)).
 
+Theorem state_low_eq_parts: forall ell s1 s2,
+    node_state_low_eq ell s1.(nodes) s2.(nodes) -> 
+    chan_state_low_eq ell s1.(chans) s2.(chans) ->
+    state_low_eq ell s1 s2.
+Proof.
+    cbv [node_state_low_eq chan_state_low_eq state_low_eq].
+    intros. eauto.
+Qed.
+
+Theorem chan_state_fe: forall ell chs1 chs2,
+    (forall h, low_eq ell chs1.[?h] chs2.[?h]) ->
+    chan_state_low_eq ell chs1 chs2.
+Proof.
+    (* shouldn't be needed after change to state loweq defs *)
+Admitted.
+
+Theorem new_secret_chan_unobs: forall ell ell' s h ,
+    ~( ell' <<L ell) ->
+    fresh_han s h ->
+    state_low_eq ell s (state_upd_chan_labeled h 
+            {| obj := new_chan; lbl := ell'|} s).
+Proof.
+    cbv [state_low_eq state_low_proj fresh_han new_chan]. intros.
+    eapply state_low_eq_parts; [cbv [state_upd_chan_labeled]; reflexivity | ].
+    eapply chan_state_fe.
+    intros. simpl. cbv [low_eq]. destruct s. cbv [RuntimeModel.chans] in *.
+    unfold low_proj.
+    destruct (dec_eq_h h h0). 
+    - rewrite <- e. rewrite H0.
+    replace 
+        ((chans .[ h <- {| obj := Some {| ms := [] |}; lbl := ell' |}]).[? h])
+        with
+        ({| obj := Some {| ms := [] |}; lbl := ell' |}) by (symmetry; eapply upd_eq).
+    destruct (top <<? ell); destruct (ell' <<? ell); (contradiction || reflexivity).
+    -  replace 
+        ( (chans .[ h <- {| obj := Some {| ms := [] |}; lbl := ell' |}]).[? h0])
+        with
+        (chans.[? h0]).
+        reflexivity. symmetry. apply upd_neq; auto. 
+Qed.
+
 Theorem unobservable_node_step: forall ell s s' e id nl n,
     s.(nodes).[? id] = nl ->
     nl.(obj) = Some n ->
@@ -159,47 +231,47 @@ Theorem unobservable_node_step: forall ell s s' e id nl n,
     ~(lbl nl <<L ell) ->
     (state_low_eq ell s s') /\ (event_low_eq ell e (empty_event e.(lbl))).
 Proof.
-    intros. inversion H1; (split; [ inversion H5 | ] ); subst_lets; crush.
-Admitted.
-(*
-    - (* WriteChannel; states loweq *) 
+    intros. inversion H1; (split; [ inversion H5 | ] ); subst_lets; crush; 
+        eauto with unobs_ev. (* handles all event-low-eq cases: *) 
+        all: separate_hyp node; separate_hyp channel.
+        all: assert (~ nlbl0 <<L ell) by congruence.
+    - (* WriteChannel *)
         assert ( ~ (lbl (chans s).[? han] <<L ell) ) by eauto using ord_trans.
         eapply state_low_eq_trans.
-        eapply (state_upd_node_unobs _ _ _ _ (node_del_rhans (rhs msg) n)
-            ltac:(eauto) ltac:(eauto) ltac:(eauto)).
-        eapply (state_upd_chan_unobs _
-            (state_upd_node id (node_del_rhans (rhs msg) n) s)
-            _ _ (chan_append ch msg)
-            ltac:(eauto) ltac:(eauto) ltac:(eauto)).
-    - (* WriteChannel; events loweq*)
-        erewrite <- (nflows_event_proj _ (n ---> msg) ltac:(eauto)).
-        unfold event_low_eq. unfold low_eq. 
-        erewrite event_low_proj_idempotent. reflexivity.
-    - (* ReadChannel; states loweq *)
-        pose proof (state_upd_chan_unobs).
-        (* This is the part of the proof where
-        the label check for destructive updates to the
-        channel are needed. See also:
-        https://github.com/project-oak/oak/issues/1197#issuecomment-712175755
-        *)
-        assert ( ~ (clbl ch <<L ell) ) by eauto using ord_trans.
+        eapply state_upd_node_unobs; eauto.
+        eapply state_chan_append_labeled_unobs; eauto.
+    - (* ReadChannel; *)
+        assert ( ~ (clbl <<L ell) ) by eauto using ord_trans.
         eapply state_low_eq_trans.
-        eapply (state_upd_node_unobs _ _ _ _ (node_get_hans n msg0) 
-            ltac:(eauto) ltac:(eauto) ltac:(eauto)).
-        eapply state_upd_chan_unobs; eauto.
-    - (* ReadChannel; events loweq *)
-        erewrite <- (nflows_event_proj _ (n <--- msg) ltac:(eauto)).
-        unfold event_low_eq. unfold low_eq.
-        erewrite event_low_proj_idempotent. reflexivity.
-    -  (* CreateChannel; states loweq *) 
-        assert ( ~ (lbl <<L ell) ) by eauto using ord_trans.
+        eapply (state_upd_node_unobs _ _ _  
+            (node_get_hans n0 msg0) ltac:(eauto)).
+        eapply (state_upd_chan_unobs _ _ _ (chan_pop ch)
+            ltac:(eauto)).
+    - (* CreateChannel *)
+        assert ( ~ (clbl <<L ell) ) by eauto using ord_trans.
         eapply state_low_eq_trans.
-        eapply (new_secret_chan_unobs _ _ _ (new_chan lbl) ltac:(eauto)); eauto.
-        eapply (state_low_eq_trans _ _ (state_upd_node id (node_add_rhan h n)
-            (state_upd_chan h (new_chan lbl) s))).
+        eapply (new_secret_chan_unobs _ clbl); eauto.
+        eapply (state_low_eq_trans _ _ 
+            (state_upd_node id (node_add_rhan h n0)
+            (state_upd_chan_labeled h {| obj := new_chan; lbl := clbl |} s))).
         eapply state_upd_node_unobs; eauto.
-        eapply (state_upd_node_unobs _ _ _ (node_add_rhan h n)); eauto.
-        eapply upd_eq.
+        eapply state_upd_node_unobs; eauto. simpl. 
+        (* wishing for erewrite upd_eq; eauto to work here.*)
+        (* I also tried making upd_eq_rev to try to get rid of the
+        need for symmetry, but that didn't seem to help *)
+        replace
+            ((nodes s .[ id <- (nodes s).[? id] <| obj ::=
+            (fun _ : option node => Some (node_add_rhan h n0)) |>]).[? id])
+            with
+            (
+                (nodes s).[? id] <| obj ::= (fun _ : option node => Some (node_add_rhan h n0)) |>
+            ).
+        eauto.
+        symmetry. eapply upd_eq.
+    - (* CreateNode *)
+        admit.
+Admitted.
+(*
     - (* CreateNode; states loweq *)
         assert ( ~ (lbl <<L ell) ) by eauto using ord_trans.
         eapply state_low_eq_trans.
@@ -231,7 +303,20 @@ Admitted.
 Qed.
 *)
 
-
+Theorem low_eq_to_unobs {A: Type}: forall ell (x1 x2: @labeled A),
+    low_eq ell x1 x2 ->
+    ~(x1.(lbl) <<L ell) ->
+    ~(x2.(lbl) <<L ell).
+Proof.
+    destruct x1, x2. cbv [low_eq low_proj RuntimeModel.lbl].
+    intros. destruct (lbl <<? ell); destruct (lbl0 <<? ell);
+        try eauto; try contradiction. 
+    inversion H. unfold not. intros.
+    pose proof top_is_top ell. 
+    pose proof (ord_anti ell top ltac:(eauto) ltac:(eauto)).
+    rewrite H5 in n.
+    pose proof top_is_top lbl. contradiction.
+Qed.
 
 Theorem step_implies_lowproj_steps_leq: forall ell s1 s1' e1,
     (step_system_ev s1 s1' e1) ->
@@ -250,13 +335,13 @@ Proof.
         destruct (nl.(lbl) <<? ell).
         * (* flowsto case *)
             inversion H_step_s1_s1'; crush; remember ((nodes s1).[?id]) as nl;
-                pose proof (state_nidx_to_proj_state_idx ell _ _ nl
-                    ltac:(eauto)) as Hn_idx_s1proj;
-                (erewrite flows_labeled_proj in Hn_idx_s1proj; eauto);
-                inversion H3; crush; subst_lets.
-                all: try replace n0 with n in * by
-                (pose proof (can_split_node_index _ _ _ _ ltac:(eauto));
-                    logical_simplify; congruence). 
+            pose proof (state_nidx_to_proj_state_idx ell _ _ nl
+                ltac:(eauto)) as Hn_idx_s1proj;
+            (erewrite flows_labeled_proj in Hn_idx_s1proj; eauto);
+            inversion H3; crush; subst_lets.
+            all: try replace n0 with n in * by
+            (pose proof (can_split_node_index _ _ _ _ ltac:(eauto));
+                logical_simplify; congruence). 
             (*
                 I can't quite get this to work. Coq complains
                 about s1 not being found in environment
@@ -278,7 +363,7 @@ Proof.
                 logical_simplify.
                 apply_all_constructors; eauto. congruence.
                 erewrite state_hidx_to_proj_state_hidx'.
-                erewrite low_projection_preserves_lbl.
+                eapply proj_labels_increase.
                 eauto.
                 (* low-equiv *)
                 subst_lets. eauto 7 with unwind.
@@ -302,6 +387,7 @@ Proof.
                 pose proof (can_split_node_index _ _ _ _ Hn_idx_s1proj);
                 logical_simplify.
                 apply_all_constructors; eauto. congruence.
+                eapply proj_preserves_fresh_han; eauto.
                 (* state loweq *)
                 subst_lets. eauto 7 with unwind.
             + (* CreateNode *)
@@ -310,6 +396,7 @@ Proof.
                 pose proof (can_split_node_index _ _ _ _ Hn_idx_s1proj);
                 logical_simplify.
                 apply_all_constructors; eauto. congruence.
+                eapply proj_preserves_fresh_nid; eauto.
                 eauto with unwind.
             +  (* Internal *)
                 do 2 eexists; split_ands; [ | | reflexivity ].
@@ -334,42 +421,15 @@ Proof.
             unfold s1''. transitivity s1'.
             symmetry. 
             eapply set_call_unobs; eauto.
-            erewrite node_low_eq_to_lbl_eq; eauto.
-            symmetry; eauto.
-            erewrite <- Heqnl in Hns1'leq. eapply Hns1'leq.
+            rewrite <- Hns1'idx in Hns1'leq.
+            eapply low_eq_to_unobs; eauto. 
+            congruence.
             pose proof (state_low_proj_loweq ell s1). 
             symmetry. transitivity s1; congruence.
             (* events leq *)
             congruence.
 Qed.
 
-Lemma separate_lableled {A} (o : option A) (l : level) (x : labeled) :
-  obj x = o -> lbl x = l -> x = Labeled _ o l.
-Proof. destruct x; cbn; congruence. Qed.
-
-Ltac separate_hyp T :=
-  repeat match goal with
-         | H : ?s = Labeled T ?o ?l |- _ =>
-           assert (obj s = o /\ lbl s = l) by (rewrite H; tauto);
-           clear H; logical_simplify
-         end.
-Ltac separate_goal := apply separate_lableled.
-
-Lemma invert_chans_state_low_proj_flowsto ell lvl s han :
-  lvl <<L ell ->
-  lvl <<L (chans (state_low_proj ell s)).[? han].(lbl) ->
-  lvl <<L (chans s).[? han].(lbl).
-Proof.
-  destruct s.
-  repeat match goal with
-         | _ => progress cbn [state_low_proj
-                               RuntimeModel.chans RuntimeModel.lbl ]
-         | _ => progress cbv [low_proj chan_state_low_proj fnd]
-         | _ => destruct_match
-         | _ => tauto
-         end.
-Qed.
-
 Theorem low_proj_steps_implies_leq_step: forall ell s s1' e1,
     (step_system_ev (state_low_proj ell s) s1' e1) ->
     (exists s2' e2,
@@ -387,31 +447,30 @@ Proof.
         pose proof (uncons_proj_node_s _ _ _ nl ltac:(eauto))
             as [n' [Hidx_n' Hproj_n']].
         destruct (nl.(lbl) <<? ell).
-        *
-          (* flowsto case*)
-            inversion H_step_projs_s1'; inversion H3;
-              (rewrite @flows_labeled_proj in *; eauto); crush;
-                lazymatch goal with
-                | |- _ <<L _ => erewrite <-low_projection_preserves_lbl; rewrite Hproj_n';
-                                solve [eauto]
+        * (* flowsto case*)
+            inversion H_step_projs_s1'; inversion H3.
+            all: rewrite @flows_labeled_proj in *; eauto; crush.
+            all: erewrite uncons_proj_node_s' in *.
+            all: lazymatch goal with
+                | H: lbl (low_proj _ _ ) <<L _ |- _ <<L _ =>
+                    rewrite <- low_proj_preserves_obs in H; eauto
                 | _ => idtac
-                end.
-        + (* WriteChannel *)
-          remember (s_set_call (state_chan_append_labeled han msg
-                                                          (state_upd_node id n'0 s)) id c') as s2''.
-          separate_hyp node.
-          eexists s2'', (lbl _ ---> msg). split.
-          { crush; try congruence;
-              [ separate_goal; eauto; congruence | ].
-            rewrite <-Hproj_n' in *.
-            eauto using invert_chans_state_low_proj_flowsto. }
-          split.
-          { crush; subst_lets; eauto with unwind. }
-          { crush. congruence. }
-        + (* ReadChannel *) admit.
-        + (* CreateChannel *) admit.
-        + (* CreateNode *) admit.
-        + (* Internal *) admit.
+            end.
+            all: separate_hyp node; separate_hyp channel.
+            + (* WriteChannel *)
+                remember (s_set_call (state_chan_append_labeled han msg
+                                        (state_upd_node id n'0 s)) id c') as s2''.
+                eexists s2'', (lbl _ ---> msg); split; [ | split].
+                { crush; try congruence. 
+                    separate_goal; eauto; congruence.
+                  rewrite <-Hproj_n' in *.
+                  eauto using invert_chans_state_low_proj_flowsto. }
+                { crush; subst_lets; eauto with unwind. }
+                { crush. congruence. }
+            + (* ReadChannel *) admit.
+            + (* CreateChannel *) admit.
+            + (* CreateNode *) admit. 
+            + (* Internal *) admit.
           (*
            + (* WriteChannel *)
                 pose proof (uncons_proj_chan_s _ _ _ _ ltac:(eauto))
@@ -486,10 +545,16 @@ Proof.
                 }
                 specialize (state_loweq_to_deref_node ell s s1' id n'
                     Hidx_n' H_leq_s_s1') as [ns1' [Hidx_s1' H_leq_n'_n2]].
-                eapply set_call_unobs. eauto.
+                eapply set_call_unobs.
+                admit.
+                (*
+                eassumption.
                 replace (lbl ns1') with (lbl n')
                     by (eapply node_low_eq_to_lbl_eq; eassumption).
-                admit.
+                replace (lbl n') with (lbl nl). eauto.
+                rewrite <- Hproj_n'.
+                eapply low_projection_preserves_lbl.
+                *)
             + (* e1 ={ell} *) assumption.
 Admitted.
 
@@ -535,13 +600,13 @@ Proof.
   all:repeat erewrite (state_low_eq_implies_node_lookup_eq ell s1 s2) in * by eauto.
   all:repeat erewrite (state_low_eq_implies_chan_lookup_eq ell s1 s2) in * by eauto.
   all:eexists; split.
-  all:lazymatch goal with
+  all:try lazymatch goal with
       | |- step_node _ _ _ _ =>
         econstructor; solve [eauto]
       | _ => subst_lets
       end.
   all:eauto using state_low_eq_projection with unwind.
-Qed.
+Admitted.
 
 Lemma step_node_ev_projection ell s1 s2 s3 id c e :
   state_low_eq ell s1 s2 ->
diff --git a/experimental/ni_coq/vfiles/RuntimeModel.v b/experimental/ni_coq/vfiles/RuntimeModel.v
index a4a5559c1d..5689736014 100644
--- a/experimental/ni_coq/vfiles/RuntimeModel.v
+++ b/experimental/ni_coq/vfiles/RuntimeModel.v
@@ -188,6 +188,10 @@ Definition node_del_rhans (hs: Ensemble handle)(n: node): node :=
 
 Definition new_chan := Some {| ms := [] |}.
 
+Definition fresh_han s h := s.(chans).[?h] = Labeled channel None top.
+
+Definition fresh_nid s id := s.(nodes).[?id] = Labeled node None top.
+
 Definition s_set_call s id c :=
     match (s.(nodes).[?id]).(obj) with
         | None => s
@@ -256,6 +260,8 @@ Inductive step_node (id: node_id): call -> state -> state -> Prop :=
     | SCreateChan s n nlbl h clbl:
         (s.(nodes).[?id]) = Labeled node (Some n) nlbl ->
             (* caller is a real node with label nlbl *)
+        fresh_han s h ->
+            (* the target handle is not in use *)
         nlbl <<L clbl ->
             let s0 := (state_upd_chan_labeled h {|
                 obj := new_chan; lbl := clbl;
@@ -266,6 +272,8 @@ Inductive step_node (id: node_id): call -> state -> state -> Prop :=
     | SCreateNode s n nlbl new_id new_lbl h:
         (s.(nodes).[?id]) = Labeled node (Some n) nlbl ->
             (* caller is a real node with label nlbl *)
+        fresh_nid s id ->
+            (* target nid is not in use *)
         nlbl <<L new_lbl ->
             (* create new node with read handle *)
         let s0 := (state_upd_node_labeled new_id {|
diff --git a/experimental/ni_coq/vfiles/Unwind.v b/experimental/ni_coq/vfiles/Unwind.v
index ca20dd9ec1..3f2d8660e1 100644
--- a/experimental/ni_coq/vfiles/Unwind.v
+++ b/experimental/ni_coq/vfiles/Unwind.v
@@ -40,14 +40,6 @@ Proof.
   inversion 1; subst.
   cbv [state_upd_node state_low_eq state_low_proj set].
   cbn [RuntimeModel.nodes RuntimeModel.chans].
-  (* this is not provable as stated; because the node-maps are functions, the
-     fact that they return the same result for every input doesn't mean they
-     obey Leibniz equality. The [low_eq] definition should probably say,
-     instead of [low_proj ell x = low_proj ell y], something like:
-
-     (forall id, nodes (low_proj_ell x) id = nodes (low_proj ell y) id)
-     /\ (forall han, chans (low_proj_ell x) han = chans (low_proj ell y) han)
-   *)
 Admitted. (* WIP // TODO *)
 
 Theorem chan_append_unwind: forall ell ch1 ch2 ch1obj ch2obj msg,
diff --git a/oak/common/BUILD b/oak/common/BUILD
index a322800f05..02daf8e389 100644
--- a/oak/common/BUILD
+++ b/oak/common/BUILD
@@ -53,16 +53,6 @@ cc_library(
     ],
 )
 
-cc_library(
-    name = "identity",
-    visibility = ["//visibility:public"],
-    deps = [
-        "//oak_abi/proto:identity_cc_proto",
-        "@com_google_absl//absl/base",
-        "@com_google_absl//absl/strings",
-    ],
-)
-
 cc_library(
     name = "nonce_generator",
     srcs = [],
diff --git a/oak_abi/proto/label.proto b/oak_abi/proto/label.proto
index 27d3bc7f73..f27ec32ff2 100644
--- a/oak_abi/proto/label.proto
+++ b/oak_abi/proto/label.proto
@@ -87,7 +87,7 @@ message TlsEndpointTag {
 
 // Policies related to identities, specified using a cryptographic public key.
 message PublicKeyIdentityTag {
-  // Public key counterpart of the private key that is used to sign an authentication challenge. 
+  // Public key counterpart of the private key that is used to sign an authentication challenge.
   // In the current implementation it is represented as a serialized Ed25519 public key.
   // https://ed25519.cr.yp.to
   bytes public_key = 1;
diff --git a/oak_derive/Cargo.lock b/oak_derive/Cargo.lock
index bcac1bdd32..6470d568b9 100644
--- a/oak_derive/Cargo.lock
+++ b/oak_derive/Cargo.lock
@@ -138,6 +138,7 @@ version = "0.1.0"
 dependencies = [
  "either",
  "hex",
+ "log",
  "oak_abi",
  "oak_derive",
  "oak_utils",
diff --git a/oak_derive/src/lib.rs b/oak_derive/src/lib.rs
index 9d1d2d01cc..66b94a0498 100644
--- a/oak_derive/src/lib.rs
+++ b/oak_derive/src/lib.rs
@@ -52,11 +52,11 @@ fn struct_impls(name: &Ident, data: &syn::DataStruct) -> TokenStream {
             .collect(),
         Fields::Unit => Vec::new(),
     };
-    let body = accessors_visit(&accessors);
+    let body = accessors_fold(&accessors);
 
     quote! {
         impl ::oak_io::handle::HandleVisit for #name {
-            fn visit<F: FnMut(&mut ::oak_io::Handle)>(&mut self, visitor: F) -> F {
+            fn fold<B>(&mut self, init: B, f: fn(B, &mut ::oak_io::Handle) -> B) -> B {
                 #body
             }
         }
@@ -67,7 +67,7 @@ fn enum_impls(name: &Ident, data: &syn::DataEnum) -> TokenStream {
     let variants: Vec<TokenStream> = data.variants.iter().map(variant_impl).collect();
     quote! {
         impl ::oak_io::handle::HandleVisit for #name {
-            fn visit<F: FnMut(&mut ::oak_io::Handle)>(&mut self, visitor: F) -> F {
+            fn fold<B>(&mut self, init: B, f: fn(B, &mut ::oak_io::Handle) -> B) -> B {
                 match self {
                     #(
                         #name::#variants,
@@ -83,7 +83,7 @@ fn variant_impl(variant: &syn::Variant) -> TokenStream {
     match &variant.fields {
         Fields::Named(fields) => {
             let fields: Vec<Ident> = fields.named.iter().flat_map(|f| f.ident.clone()).collect();
-            let body = accessors_visit(&fields);
+            let body = accessors_fold(&fields);
             quote! {
                 #variant_ident { #( #fields ),* } => {
                     #body
@@ -98,7 +98,7 @@ fn variant_impl(variant: &syn::Variant) -> TokenStream {
                 .enumerate()
                 .map(|(i, _)| format_ident!("_{}", i))
                 .collect();
-            let body = accessors_visit(&accessors);
+            let body = accessors_fold(&accessors);
             quote! {
                 #variant_ident( #( #accessors ),* ) => {
                     #body
@@ -106,17 +106,17 @@ fn variant_impl(variant: &syn::Variant) -> TokenStream {
             }
         }
         Fields::Unit => quote! {
-            #variant_ident => visitor
+            #variant_ident => init
         },
     }
 }
 
-fn accessors_visit<T: ToTokens>(accessors: &[T]) -> TokenStream {
+fn accessors_fold<T: ToTokens>(accessors: &[T]) -> TokenStream {
     quote! {
-        let mut _v = visitor;
+        let accumulator = init;
         #(
-            _v  = #accessors.visit(_v);
+            let accumulator = #accessors.fold(accumulator, f);
         )*
-        _v
+        accumulator
     }
 }
diff --git a/oak_io/Cargo.lock b/oak_io/Cargo.lock
index 9fcf522214..6fc8fde95a 100644
--- a/oak_io/Cargo.lock
+++ b/oak_io/Cargo.lock
@@ -144,6 +144,7 @@ dependencies = [
  "assert_matches",
  "either",
  "hex",
+ "log",
  "oak_abi",
  "oak_derive",
  "oak_utils",
diff --git a/oak_io/Cargo.toml b/oak_io/Cargo.toml
index 7e4cec5ece..26c20b87c2 100644
--- a/oak_io/Cargo.toml
+++ b/oak_io/Cargo.toml
@@ -14,6 +14,7 @@ oak_derive = { path = "../oak_derive" }
 prost = "*"
 prost-types = "*"
 either = "*"
+log = "*"
 
 [dev-dependencies]
 assert_matches = "*"
diff --git a/oak_io/src/handle.rs b/oak_io/src/handle.rs
index a41ae7a576..efdf2a53de 100644
--- a/oak_io/src/handle.rs
+++ b/oak_io/src/handle.rs
@@ -16,6 +16,7 @@
 include!(concat!(env!("OUT_DIR"), "/oak.handle.rs"));
 
 use crate::OakError;
+use log::error;
 use oak_abi::Handle;
 
 /// Wrapper for a handle to the read half of a channel.
@@ -82,9 +83,8 @@ impl From<Handle> for WriteHandle {
 /// }
 ///
 /// impl HandleVisit for Thing {
-///     fn visit<F: FnMut(&mut Handle)>(&mut self, mut visitor: F) -> F {
-///         visitor(&mut self.handle);
-///         visitor
+///     fn fold<B>(&mut self, init: B, mut f: fn(B, &mut Handle) -> B) -> B {
+///         f(init, &mut self.handle)
 ///     }
 /// }
 /// ```
@@ -92,7 +92,7 @@ pub trait HandleVisit {
     /// Invokes the provided closure on every handle contained in `self`.
     ///
     /// The mutable reference allows modifying the handles.
-    fn visit<F: FnMut(&mut Handle)>(&mut self, visitor: F) -> F;
+    fn fold<B>(&mut self, init: B, f: fn(B, &mut Handle) -> B) -> B;
 }
 
 /// Return all handles in `T`.
@@ -112,9 +112,8 @@ pub trait HandleVisit {
 ///     handle: Handle,
 /// }
 /// # impl HandleVisit for Thing {
-/// #   fn visit<F: FnMut(&mut Handle)>(&mut self, mut visitor: F) -> F {
-/// #     visitor(&mut self.handle);
-/// #     visitor
+/// #   fn fold<B>(&mut self, init: B, f: fn(B, &mut Handle) -> B) -> B {
+/// #       f(init, &mut self.handle)
 /// #   }
 /// # }
 ///
@@ -125,13 +124,11 @@ pub trait HandleVisit {
 /// assert_eq!(handles, vec![42]);
 /// ```
 pub fn extract_handles<T: HandleVisit>(msg: &mut T) -> Vec<Handle> {
-    let mut handles = Vec::new();
-    // TODO(#1599): Remove the `let _` when the underlying issue is fixed.
-    let _ = msg.visit(|handle: &mut Handle| {
+    msg.fold(Vec::new(), |mut handles, handle| {
         handles.push(*handle);
         *handle = oak_abi::INVALID_HANDLE;
-    });
-    handles
+        handles
+    })
 }
 
 /// Inject handles into a message.
@@ -153,9 +150,8 @@ pub fn extract_handles<T: HandleVisit>(msg: &mut T) -> Vec<Handle> {
 ///     handle: Handle,
 /// }
 /// # impl HandleVisit for Thing {
-/// #   fn visit<F: FnMut(&mut Handle)>(&mut self, mut visitor: F) -> F {
-/// #     visitor(&mut self.handle);
-/// #     visitor
+/// #   fn fold<B>(&mut self, init: B, f: fn(B, &mut Handle) -> B) -> B {
+/// #       f(init, &mut self.handle)
 /// #   }
 /// # }
 ///
@@ -167,20 +163,24 @@ pub fn extract_handles<T: HandleVisit>(msg: &mut T) -> Vec<Handle> {
 /// assert_eq!(thing, Thing { handle: 42 });
 /// ```
 pub fn inject_handles<T: HandleVisit>(msg: &mut T, handles: &[Handle]) -> Result<(), OakError> {
-    let mut handles = handles.iter();
-    let mut result = Ok(());
-    // TODO(#1599): Remove the `let _` when the underlying issue is fixed.
-    let _ = msg.visit(|handle| {
-        if let Some(to_inject) = handles.next() {
-            *handle = *to_inject;
+    msg.fold(Ok(handles.iter()), |handles, handle| {
+        let mut handles = handles?;
+        let to_inject = handles.next().ok_or_else(|| {
+            error!("Not enough handles provided to populate message");
+            OakError::ProtobufDecodeError(None)
+        })?;
+        *handle = *to_inject;
+        Ok(handles)
+    })
+    // Check that there are no remaining handles
+    .and_then(|mut remaining_handles| {
+        if remaining_handles.next().is_some() {
+            error!("Too many handles provided for message",);
+            Err(OakError::ProtobufDecodeError(None))
         } else {
-            result = Err(OakError::ProtobufDecodeError(None));
+            Ok(())
         }
-    });
-    if handles.next().is_some() {
-        result = Err(OakError::ProtobufDecodeError(None));
-    }
-    result
+    })
 }
 
 // A default implementation of the HandleVisit trait that does nothing
@@ -189,8 +189,8 @@ macro_rules! handle_visit_blanket_impl {
     ($($t:ty),+) => {
         $(
             impl HandleVisit for $t {
-                fn visit<F: FnMut(&mut Handle)>(&mut self, visitor: F) -> F {
-                    visitor
+                fn fold<B>(&mut self, init: B, _: fn(B, &mut Handle) -> B) -> B {
+                    init
                 }
             }
         )+
@@ -220,27 +220,26 @@ pub use oak_derive::HandleVisit;
 
 // Optional fields
 impl<T: HandleVisit> HandleVisit for Option<T> {
-    fn visit<F: FnMut(&mut Handle)>(&mut self, visitor: F) -> F {
+    fn fold<B>(&mut self, init: B, f: fn(B, &mut Handle) -> B) -> B {
         if let Some(inner) = self {
-            inner.visit(visitor)
+            inner.fold(init, f)
         } else {
-            visitor
+            init
         }
     }
 }
 
 // For repeated fields.
 impl<T: HandleVisit> HandleVisit for Vec<T> {
-    fn visit<F: FnMut(&mut Handle)>(&mut self, visitor: F) -> F {
-        self.iter_mut()
-            .fold(visitor, |visitor, item| item.visit(visitor))
+    fn fold<B>(&mut self, init: B, f: fn(B, &mut Handle) -> B) -> B {
+        self.iter_mut().fold(init, |init, item| item.fold(init, f))
     }
 }
 
 // For recursive messages.
 impl<T: HandleVisit> HandleVisit for Box<T> {
-    fn visit<F: FnMut(&mut Handle)>(&mut self, visitor: F) -> F {
-        self.as_mut().visit(visitor)
+    fn fold<B>(&mut self, init: B, f: fn(B, &mut Handle) -> B) -> B {
+        self.as_mut().fold(init, f)
     }
 }
 
@@ -252,13 +251,13 @@ impl<T: HandleVisit> HandleVisit for Box<T> {
 impl<K: Ord + core::hash::Hash, V: HandleVisit, S> HandleVisit
     for std::collections::HashMap<K, V, S>
 {
-    fn visit<F: FnMut(&mut Handle)>(&mut self, visitor: F) -> F {
+    fn fold<B>(&mut self, init: B, f: fn(B, &mut Handle) -> B) -> B {
         let mut entries: Vec<(&K, &mut V)> = self.iter_mut().collect();
         // Can be unstable because keys are guaranteed to be unique.
         entries.sort_unstable_by_key(|&(k, _)| k);
         entries
             .into_iter()
             .map(|(_, v)| v)
-            .fold(visitor, |visitor, value| value.visit(visitor))
+            .fold(init, |init, value| value.fold(init, f))
     }
 }
diff --git a/oak_io/src/receiver.rs b/oak_io/src/receiver.rs
index 34f543865a..70c712b5ba 100644
--- a/oak_io/src/receiver.rs
+++ b/oak_io/src/receiver.rs
@@ -59,9 +59,8 @@ impl<T: Decodable> From<ReadHandle> for Receiver<T> {
 }
 
 impl<T: Decodable> crate::handle::HandleVisit for Receiver<T> {
-    fn visit<F: FnMut(&mut crate::Handle)>(&mut self, mut visitor: F) -> F {
-        visitor(&mut self.handle.handle);
-        visitor
+    fn fold<B>(&mut self, init: B, f: fn(B, &mut crate::Handle) -> B) -> B {
+        f(init, &mut self.handle.handle)
     }
 }
 
diff --git a/oak_io/src/sender.rs b/oak_io/src/sender.rs
index f24f571a46..fd5be34332 100644
--- a/oak_io/src/sender.rs
+++ b/oak_io/src/sender.rs
@@ -42,9 +42,8 @@ impl<T: Encodable> Sender<T> {
 }
 
 impl<T: Encodable> crate::handle::HandleVisit for Sender<T> {
-    fn visit<F: FnMut(&mut crate::Handle)>(&mut self, mut visitor: F) -> F {
-        visitor(&mut self.handle.handle);
-        visitor
+    fn fold<B>(&mut self, init: B, f: fn(B, &mut crate::Handle) -> B) -> B {
+        f(init, &mut self.handle.handle)
     }
 }
 
diff --git a/oak_loader/Cargo.lock b/oak_loader/Cargo.lock
index 2b6598ea6b..e4d07f6e6f 100644
--- a/oak_loader/Cargo.lock
+++ b/oak_loader/Cargo.lock
@@ -718,6 +718,7 @@ version = "0.1.0"
 dependencies = [
  "either",
  "hex",
+ "log",
  "oak_abi",
  "oak_derive",
  "oak_utils",
@@ -1240,9 +1241,9 @@ dependencies = [
 
 [[package]]
 name = "serde_json"
-version = "1.0.58"
+version = "1.0.59"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a230ea9107ca2220eea9d46de97eddcb04cd00e92d13dda78e478dd33fa82bd4"
+checksum = "dcac07dbffa1c65e7f816ab9eba78eb142c6d44410f4eeba1e26e4f5dfa56b95"
 dependencies = [
  "itoa",
  "ryu",
diff --git a/oak_runtime/Cargo.lock b/oak_runtime/Cargo.lock
index 6fc077d234..3a371d522c 100644
--- a/oak_runtime/Cargo.lock
+++ b/oak_runtime/Cargo.lock
@@ -730,6 +730,7 @@ version = "0.1.0"
 dependencies = [
  "either",
  "hex",
+ "log",
  "oak_abi",
  "oak_derive",
  "oak_utils",
diff --git a/oak_services/Cargo.lock b/oak_services/Cargo.lock
index 65e7726c9b..0f9dc97f64 100644
--- a/oak_services/Cargo.lock
+++ b/oak_services/Cargo.lock
@@ -166,6 +166,7 @@ version = "0.1.0"
 dependencies = [
  "either",
  "hex",
+ "log",
  "oak_abi",
  "oak_derive",
  "oak_utils",
diff --git a/oak_utils/src/lib.rs b/oak_utils/src/lib.rs
index a4ba1ca909..ee90e74f2e 100644
--- a/oak_utils/src/lib.rs
+++ b/oak_utils/src/lib.rs
@@ -70,26 +70,31 @@ impl prost_build::ServiceGenerator for OakServiceGenerator {
         });
 
         let dispatcher_name = format_ident!("{}Dispatcher", service.name);
-        let dispatcher_methods = service.methods.iter().map(|method| {
+        let dispatcher_invocable_methods = service.methods.iter().map(|method| {
             let method_name = format_ident!("{}", method.name);
-            let method_name_string = format!("/{}.{}/{}", service.package, service.proto_name, method.proto_name);
-            // Figure out which generic function applies.
-            let handle_invocation = match (method.client_streaming, method.server_streaming) {
+            let method_name_string = format!(
+                "/{}.{}/{}",
+                service.package, service.proto_name, method.proto_name
+            );
+            // Figure out which `ServerMethod` variant applies.
+            let invocable_method = match (method.client_streaming, method.server_streaming) {
                 (false, false) => quote! {
-                    #oak_package::grpc::handle_req_rsp(|r| (self.0).#method_name(r), req, writer)
+                    Some(&#oak_package::grpc::ServerMethod::UnaryUnary(T::#method_name))
                 },
                 (false, true) => quote! {
-                    #oak_package::grpc::handle_req_stream(|r, w| (self.0).#method_name(r, w), req, writer)
+                    // The response type is not actually used in the method signature, so we need to manually specify a placeholder.
+                    Some(&#oak_package::grpc::ServerMethod::<_, _, ()>::UnaryStream(T::#method_name))
                 },
                 (true, false) => quote! {
-                    #oak_package::grpc::handle_stream_rsp(|rr| (self.0).#method_name(rr), req, writer)
+                    Some(&#oak_package::grpc::ServerMethod::StreamUnary(T::#method_name))
                 },
                 (true, true) => quote! {
-                    #oak_package::grpc::handle_stream_stream(|rr, w| (self.0).#method_name(rr, w), req, writer)
+                    // The response type is not actually used in the method signature, so we need to manually specify a placeholder.
+                    Some(&#oak_package::grpc::ServerMethod::<_, _, ()>::StreamStream(T::#method_name))
                 },
             };
             quote! {
-                #method_name_string => #handle_invocation
+                #method_name_string => #invocable_method
             }
         });
 
@@ -133,6 +138,13 @@ impl prost_build::ServiceGenerator for OakServiceGenerator {
                 pub fn new(node: T) -> #dispatcher_name<T> {
                     #dispatcher_name(node)
                 }
+
+                pub fn server_method(method_name: &str) -> Option<&dyn #oak_package::grpc::Invocable<T>> {
+                    match method_name {
+                        #(#dispatcher_invocable_methods,)*
+                        _ => None
+                    }
+                }
             }
 
             impl <T: #service_name + Default> Default for #dispatcher_name<T> {
@@ -151,12 +163,10 @@ impl prost_build::ServiceGenerator for OakServiceGenerator {
 
             #[allow(clippy::unit_arg)]
             impl <T: #service_name> #oak_package::grpc::ServerNode for #dispatcher_name<T> {
-                fn invoke(&mut self, method: &str, req: &[u8], writer: #oak_package::grpc::ChannelResponseWriter) {
-                    match method {
-                        #(#dispatcher_methods,)*
-                        _ => {
-                            ::log::error!("unknown method name: {}", method);
-                        }
+                fn invoke(&mut self, method_name: &str, req: &[u8], writer: #oak_package::grpc::ChannelResponseWriter) {
+                    match #dispatcher_name::<T>::server_method(method_name) {
+                        Some(server_method) => server_method.invoke(&mut self.0, req, writer),
+                        None => ::log::error!("unknown method name: {}", method_name),
                     }
                 }
             }
diff --git a/sdk/Cargo.lock b/sdk/Cargo.lock
index 86706d966c..1833a9c5bf 100644
--- a/sdk/Cargo.lock
+++ b/sdk/Cargo.lock
@@ -828,6 +828,7 @@ version = "0.1.0"
 dependencies = [
  "either",
  "hex",
+ "log",
  "oak_abi",
  "oak_derive",
  "oak_utils",
diff --git a/sdk/deny.toml b/sdk/deny.toml
index b338f70b88..158d044dc8 100644
--- a/sdk/deny.toml
+++ b/sdk/deny.toml
@@ -23,19 +23,6 @@ ignore = [
 multiple-versions = "deny"
 wildcards = "allow"
 
-# TODO(#1270): Remove when no longer needed by tonic and rustls.
-[[bans.skip]]
-name = "base64"
-version = "=0.11.0"
-
-[[bans.skip]]
-name = "tokio-rustls"
-version = "=0.13.1"
-
-[[bans.skip]]
-name = "rustls"
-version = "=0.17.0"
-
 [[bans.skip]]
 name = "pin-project"
 version = "=0.4.22"
diff --git a/sdk/rust/oak/src/grpc/mod.rs b/sdk/rust/oak/src/grpc/mod.rs
index 8e7f47df96..70554f9a12 100644
--- a/sdk/rust/oak/src/grpc/mod.rs
+++ b/sdk/rust/oak/src/grpc/mod.rs
@@ -295,74 +295,71 @@ where
     Ok(rsp)
 }
 
-/// Generic function that handles request deserialization and response
-/// serialization (and sending down a channel) for a function that handles a
-/// request/response pair.
-///
-/// Panics if [de-]serialization or channel operations fail.
-pub fn handle_req_rsp<C, R, Q>(mut node_fn: C, req: &[u8], writer: ChannelResponseWriter)
-where
-    C: FnMut(R) -> Result<Q>,
-    R: prost::Message + Default,
-    Q: prost::Message,
-{
-    let r = R::decode(req).expect("Failed to parse request protobuf message");
-    let result = match node_fn(r) {
-        Ok(rsp) => writer.write(&rsp, WriteMode::Close),
-        Err(status) => writer.close(Err(status)),
-    };
-    if let Err(e) = result {
-        panic!("Failed to process response: {:?}", e)
-    }
+/// Trait implemented by all server method variants, applied to a server receiver instance having
+/// concrete type `T`.
+pub trait Invocable<T> {
+    /// Generic function that handles request deserialization and response serialization (and
+    /// sending down a channel) for a function that handles a request / response pair (either unary
+    /// or streaming).
+    ///
+    /// Panics if [de-]serialization or channel operations fail.
+    fn invoke(&self, target: &mut T, req: &[u8], writer: ChannelResponseWriter);
 }
 
-/// Generic function that handles request deserialization and response
-/// serialization (and sending down a channel) for a function that handles a
-/// request and streams responses.
+/// Enum with variants for all combinations of {request, response} × {unary , streaming}, each
+/// containing a pointer to the function of the appropriate type defined on a service
+/// implementation.
 ///
-/// Panics if [de-]serialization or channel operations fail.
-pub fn handle_req_stream<C, R>(mut node_fn: C, req: &[u8], writer: ChannelResponseWriter)
-where
-    C: FnMut(R, ChannelResponseWriter),
-    R: prost::Message + Default,
-{
-    let r = R::decode(req).expect("Failed to parse request protobuf message");
-    node_fn(r, writer)
-}
-
-/// Generic function that handles request deserialization and response
-/// serialization (and sending down a channel) for a function that handles a
-/// stream of requests to produce a response.
+/// The functions are "uncurried", i.e. they include an explicit parameter for the receiver type,
+/// which corresponds to `self` in the method definition.
 ///
-/// Panics if [de-]serialization or channel operations fail.
-pub fn handle_stream_rsp<C, R, Q>(mut node_fn: C, req: &[u8], writer: ChannelResponseWriter)
-where
-    C: FnMut(Vec<R>) -> Result<Q>,
-    R: prost::Message + Default,
-    Q: prost::Message + Default,
-{
-    // TODO(#97): better client-side streaming
-    let rr = vec![R::decode(req).expect("Failed to parse request protobuf message")];
-    let result = match node_fn(rr) {
-        Ok(rsp) => writer.write(&rsp, WriteMode::Close),
-        Err(status) => writer.close(Err(status)),
-    };
-    if let Err(e) = result {
-        panic!("Failed to process response: {:?}", e)
-    }
+/// Note that the variants with response stream do not make use of the type parameter `Q`, so this
+/// must be manually specified when creating one of those instances if the compiler cannot infer it
+/// from the context.
+pub enum ServerMethod<T, R, Q> {
+    UnaryUnary(fn(&mut T, R) -> Result<Q>),
+    UnaryStream(fn(&mut T, R, ChannelResponseWriter)),
+    StreamUnary(fn(&mut T, Vec<R>) -> Result<Q>),
+    StreamStream(fn(&mut T, Vec<R>, ChannelResponseWriter)),
 }
 
-/// Generic function that handles request deserialization and response
-/// serialization (and sending down a channel) for a function that handles a
-/// stream of requests to produce a stream of responses.
-///
-/// Panics if [de-]serialization or channel operations fail.
-pub fn handle_stream_stream<C, R>(mut node_fn: C, req: &[u8], writer: ChannelResponseWriter)
+impl<T, R, Q> Invocable<T> for ServerMethod<T, R, Q>
 where
-    C: FnMut(Vec<R>, ChannelResponseWriter),
     R: prost::Message + Default,
+    Q: prost::Message,
 {
-    // TODO(#97): better client-side streaming
-    let rr = vec![R::decode(req).expect("Failed to parse request protobuf message")];
-    node_fn(rr, writer)
+    fn invoke(&self, target: &mut T, req: &[u8], writer: ChannelResponseWriter) {
+        match self {
+            ServerMethod::UnaryUnary(server_method) => {
+                let r = R::decode(req).expect("Failed to parse request protobuf message");
+                let result = match server_method(target, r) {
+                    Ok(rsp) => writer.write(&rsp, WriteMode::Close),
+                    Err(status) => writer.close(Err(status)),
+                };
+                if let Err(e) = result {
+                    panic!("Failed to process response: {:?}", e)
+                }
+            }
+            ServerMethod::UnaryStream(server_method) => {
+                let r = R::decode(req).expect("Failed to parse request protobuf message");
+                server_method(target, r, writer)
+            }
+            ServerMethod::StreamUnary(server_method) => {
+                // TODO(#97): better client-side streaming
+                let rr = vec![R::decode(req).expect("Failed to parse request protobuf message")];
+                let result = match server_method(target, rr) {
+                    Ok(rsp) => writer.write(&rsp, WriteMode::Close),
+                    Err(status) => writer.close(Err(status)),
+                };
+                if let Err(e) = result {
+                    panic!("Failed to process response: {:?}", e)
+                }
+            }
+            ServerMethod::StreamStream(server_method) => {
+                // TODO(#97): better client-side streaming
+                let rr = vec![R::decode(req).expect("Failed to parse request protobuf message")];
+                server_method(target, rr, writer)
+            }
+        }
+    }
 }


Test patch:
diff --git a/examples/abitest/client/cpp/BUILD b/examples/abitest/client/cpp/BUILD
index 0b9c54d398..2c5fc32cb9 100644
--- a/examples/abitest/client/cpp/BUILD
+++ b/examples/abitest/client/cpp/BUILD
@@ -66,9 +66,11 @@ cc_library(
     hdrs = ["httptest.h"],
     deps = [
         ":httplib_config",
-        "//oak/common:identity",
         "//oak/common:label",
+        "//oak_abi/proto:identity_cc_proto",
         "@com_github_google_glog//:glog",
+        "@com_google_absl//absl/base",
+        "@com_google_absl//absl/strings",
     ],
 )
 
diff --git a/examples/abitest/module_0/rust/tests/integration_test.rs b/examples/abitest/module_0/rust/tests/integration_test.rs
index 56e366f096..116e2d23cb 100644
--- a/examples/abitest/module_0/rust/tests/integration_test.rs
+++ b/examples/abitest/module_0/rust/tests/integration_test.rs
@@ -58,7 +58,7 @@ async fn setup() -> (
     let runtime =
         oak_runtime::configure_and_run(config).expect("unable to configure runtime with test wasm");
 
-    let (channel, interceptor) = oak_tests::channel_and_interceptor().await;
+    let (channel, interceptor) = oak_tests::public_channel_and_interceptor().await;
     let client = OakAbiTestServiceClient::with_interceptor(channel, interceptor);
 
     (runtime, client)
diff --git a/examples/aggregator/module/rust/tests/integration_test.rs b/examples/aggregator/module/rust/tests/integration_test.rs
index e37fc8511c..a454c6f80a 100644
--- a/examples/aggregator/module/rust/tests/integration_test.rs
+++ b/examples/aggregator/module/rust/tests/integration_test.rs
@@ -55,7 +55,7 @@ async fn test_aggregator() {
     )
     .expect("Unable to configure runtime with test wasm!");
 
-    let (channel, interceptor) = oak_tests::channel_and_interceptor().await;
+    let (channel, interceptor) = oak_tests::public_channel_and_interceptor().await;
     let mut client = AggregatorClient::with_interceptor(channel, interceptor);
 
     for i in 0..SAMPLE_THRESHOLD as u32 {
diff --git a/examples/chat/module/rust/tests/integration_test.rs b/examples/chat/module/rust/tests/integration_test.rs
index b44d29f68a..ece65d12b6 100644
--- a/examples/chat/module/rust/tests/integration_test.rs
+++ b/examples/chat/module/rust/tests/integration_test.rs
@@ -149,7 +149,7 @@ impl<'a> Chatter<'a> {
             user_handle,
             base64::encode(&room_key_pair.pkcs8_public_key())
         );
-        let (channel, interceptor) = oak_tests::channel_and_interceptor().await;
+        let (channel, interceptor) = oak_tests::public_channel_and_interceptor().await;
         // TODO(#1357): Use key pair to authenticate this client and label requests.
         let client = ChatClient::with_interceptor(channel, interceptor);
         Chatter {
diff --git a/examples/hello_world/module/rust/tests/integration_test.rs b/examples/hello_world/module/rust/tests/integration_test.rs
index 77a2c9c16e..be0281fbc9 100644
--- a/examples/hello_world/module/rust/tests/integration_test.rs
+++ b/examples/hello_world/module/rust/tests/integration_test.rs
@@ -28,7 +28,7 @@ async fn test_say_hello() {
     let runtime = oak_tests::run_single_module_default(MODULE_WASM_FILE_NAME)
         .expect("Unable to configure runtime with test wasm!");
 
-    let (channel, interceptor) = oak_tests::channel_and_interceptor().await;
+    let (channel, interceptor) = oak_tests::public_channel_and_interceptor().await;
     let mut client = HelloWorldClient::with_interceptor(channel, interceptor);
 
     let req = HelloRequest {
diff --git a/examples/private_set_intersection/module/rust/tests/integration_test.rs b/examples/private_set_intersection/module/rust/tests/integration_test.rs
index d40d5ff459..77a612d5fa 100644
--- a/examples/private_set_intersection/module/rust/tests/integration_test.rs
+++ b/examples/private_set_intersection/module/rust/tests/integration_test.rs
@@ -31,7 +31,7 @@ async fn test_set_intersection() {
     let runtime = oak_tests::run_single_module_default(MODULE_WASM_FILE_NAME)
         .expect("Unable to configure runtime with test wasm!");
 
-    let (channel, interceptor) = oak_tests::channel_and_interceptor().await;
+    let (channel, interceptor) = oak_tests::public_channel_and_interceptor().await;
     let mut client = PrivateSetIntersectionClient::with_interceptor(channel, interceptor);
 
     let req = SubmitSetRequest {
diff --git a/examples/running_average/module/rust/tests/integration_test.rs b/examples/running_average/module/rust/tests/integration_test.rs
index 7227ff954d..6c7b1255a0 100644
--- a/examples/running_average/module/rust/tests/integration_test.rs
+++ b/examples/running_average/module/rust/tests/integration_test.rs
@@ -34,7 +34,7 @@ async fn test_running_average() {
     let runtime = oak_tests::run_single_module_default(MODULE_WASM_FILE_NAME)
         .expect("Unable to configure runtime with test wasm!");
 
-    let (channel, interceptor) = oak_tests::channel_and_interceptor().await;
+    let (channel, interceptor) = oak_tests::public_channel_and_interceptor().await;
     let mut client = RunningAverageClient::with_interceptor(channel, interceptor);
 
     submit_sample(&mut client, 100).await;
diff --git a/examples/translator/module/rust/tests/integration_test.rs b/examples/translator/module/rust/tests/integration_test.rs
index a32cf3199e..29e0dd2e05 100644
--- a/examples/translator/module/rust/tests/integration_test.rs
+++ b/examples/translator/module/rust/tests/integration_test.rs
@@ -27,7 +27,7 @@ async fn test_translate() {
     let runtime = oak_tests::run_single_module(MODULE_WASM_FILE_NAME, "grpc_oak_main")
         .expect("Unable to configure runtime with test wasm!");
 
-    let (channel, interceptor) = oak_tests::channel_and_interceptor().await;
+    let (channel, interceptor) = oak_tests::public_channel_and_interceptor().await;
     let mut client = TranslatorClient::with_interceptor(channel, interceptor);
 
     let req = TranslateRequest {
diff --git a/examples/trusted_database/module/rust/tests/integration_test.rs b/examples/trusted_database/module/rust/tests/integration_test.rs
index f5b178ec48..adc97faff8 100644
--- a/examples/trusted_database/module/rust/tests/integration_test.rs
+++ b/examples/trusted_database/module/rust/tests/integration_test.rs
@@ -130,7 +130,7 @@ async fn test_trusted_database() {
     let runtime =
         oak_runtime::configure_and_run(config).expect("Couldn't configure runtime with test wasm");
 
-    let (channel, interceptor) = oak_tests::channel_and_interceptor().await;
+    let (channel, interceptor) = oak_tests::public_channel_and_interceptor().await;
     let mut client = TrustedDatabaseClient::with_interceptor(channel, interceptor);
 
     // Test nearest point of interest.
diff --git a/oak_derive/tests/visit.rs b/oak_derive/tests/visit.rs
index 716c7489bf..1380334ed7 100644
--- a/oak_derive/tests/visit.rs
+++ b/oak_derive/tests/visit.rs
@@ -20,9 +20,8 @@ use oak_io::{handle::HandleVisit, Handle};
 struct Visited(Handle);
 
 impl HandleVisit for Visited {
-    fn visit<F: FnMut(&mut Handle)>(&mut self, mut f: F) -> F {
-        f(&mut self.0);
-        f
+    fn fold<B>(&mut self, init: B, f: fn(B, &mut Handle) -> B) -> B {
+        f(init, &mut self.0)
     }
 }
 
@@ -127,14 +126,9 @@ mod enums {
     }
 }
 
-// Asserts that `t` is visited exactly `count` times when calling `HandleVisit::visit`.
-fn assert_visit<T: HandleVisit>(mut t: T, count: usize) {
-    let mut counter = 0;
+// Asserts that `t` is visited exactly `expected` times when calling [`HandleVisit::fold`].
+fn assert_visit<T: HandleVisit>(mut t: T, expected: usize) {
+    let count = t.fold(0, |count, _| count + 1);
 
-    // TODO(#1599): Remove the `let _` when the underlying issue is fixed.
-    let _ = t.visit(|_| {
-        counter += 1;
-    });
-
-    assert_eq!(counter, count);
+    assert_eq!(count, expected);
 }
diff --git a/sdk/rust/oak_tests/src/lib.rs b/sdk/rust/oak_tests/src/lib.rs
index d45899fca0..f3d452c979 100644
--- a/sdk/rust/oak_tests/src/lib.rs
+++ b/sdk/rust/oak_tests/src/lib.rs
@@ -197,9 +197,9 @@ fn create_http_config() -> Option<oak_runtime::HttpConfiguration> {
     Some(oak_runtime::HttpConfiguration { tls_config })
 }
 
-/// Build a channel and interceptor suitable for building a client that connects
-/// to a Runtime under test.
-pub async fn channel_and_interceptor() -> (Channel, impl Into<tonic::Interceptor>) {
+/// Build a labeled channel and interceptor suitable for building a client that
+/// connects to a Runtime under test.
+pub async fn channel_and_interceptor(label: &Label) -> (Channel, impl Into<tonic::Interceptor>) {
     // Build a channel that connects to the Runtime under test.
     let uri = RUNTIME_URI.parse().expect("Error parsing URI");
     let tls_config = ClientTlsConfig::new()
@@ -235,17 +235,23 @@ pub async fn channel_and_interceptor() -> (Channel, impl Into<tonic::Interceptor
 
     // Build an interceptor that will attach a public-untrusted Oak label to
     // every gRPC request.
-    let mut label = Vec::new();
-    Label::public_untrusted()
-        .encode(&mut label)
+    let mut encoded_label = Vec::new();
+    label
+        .encode(&mut encoded_label)
         .expect("Error encoding label");
     let interceptor = move |mut request: Request<()>| {
         request.metadata_mut().insert_bin(
             oak_abi::OAK_LABEL_GRPC_METADATA_KEY,
-            MetadataValue::from_bytes(label.as_ref()),
+            MetadataValue::from_bytes(encoded_label.as_ref()),
         );
         Ok(request)
     };
 
     (channel, interceptor)
 }
+
+/// Build a public-untrusted channel and interceptor suitable for building a
+/// client that connects to a Runtime under test.
+pub async fn public_channel_and_interceptor() -> (Channel, impl Into<tonic::Interceptor>) {
+    channel_and_interceptor(&Label::public_untrusted()).await
+}