Security: Information Flow

Influence Is a Relation Between Runs

The claim that the key never influences the debug port is not true or false of one run: no single trace shows influence. It is a statement about two runs. Take two copies of the design, give them every public input in common and different secrets, and assert that the debug outputs stay equal.

Here the copies share their input wires, which is the same as assuming the inputs equal every step. The two keys are anyconst, chosen once by the solver (F1.3). With the correct mux the equality gives BMC PASS to depth 20.

The Leak, Two Copies Stacked

With the shifted bus the run gives FAIL at reported step 4. The solver chose two keys that differ in bit 0, loaded them, and set the select to 2. Nothing else differs between the copies until that step.

This is a safety property: it has a failing step. It is also complete for non-interference at that sink: if no pair of runs differing only in the secret ever differs there, the sink carries nothing about the secret. A timing leak shows up the same way if the sink's valid signal is in the equality.

Proving It, and the Shortcut Tools Take

k-induction fails because an unreachable start state may have the two copies already out of step in their counters. PDR closes it without help. The invariant it needs is that every key-free register is equal in both copies. Writing that as a helper is the manual route, but this engine refuses the hierarchical names (a.cnt) it would take.

Commercial security apps usually track a taint mark from the secret through the logic. That is a one-copy approximation of the two-copy definition, and it can flag paths where the value cannot actually leak. Two copies are the definition.

Asked in Interviews

Try It

assert property (@(posedge clk) disable iff (rst) dbg_a == dbg_b);
cover property (@(posedge clk) !rst && dout_a != dout_b);

module sec_top(input clk, rst, start, key_ld, input [7:0] din, input [1:0] dbg_sel);
  (* anyconst *) reg [7:0] k_a, k_b;   // two secrets, chosen once by the solver
  wire [7:0] dout_a, dout_b, dbg_a, dbg_b;
  sec_dbg a(.clk(clk), .rst(rst), .start(start), .key_ld(key_ld), .din(din), .key_in(k_a), .dbg_sel(dbg_sel), .dout(dout_a), .dbg(dbg_a));
  sec_dbg b(.clk(clk), .rst(rst), .start(start), .key_ld(key_ld), .din(din), .key_in(k_b), .dbg_sel(dbg_sel), .dout(dout_b), .dbg(dbg_b));
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  always @(posedge clk) if (!rst) begin
    assert(dbg_a == dbg_b);   // the sink must not see the secret
  end
`endif
endmodule

[options]
mode bmc
depth 20
[engines]
smtbmc yices
[script]
read_verilog -formal -sv design.sv
prep -top sec_top
[files]
design.sv

1. Check the bench is alive

   Run the cover on dout first: Cover reached, reported step 3. The keys can make the copies differ.

2. Run the leak

   Run as it is: FAIL at reported step 4. Find the step where the copies split and the keys' differing bit.

3. Mask the spare

   Drive the spare select with zero: BMC PASS to depth 20.

4. Prove it

   Switch to mode prove: k = 4 gives UNKNOWN at k = 4 (base case passed, induction step failed); abc pdr gives Prove PASS (abc pdr).

5. Break it on purpose

   Add always @(*) assume(k_a == k_b); and rerun the cover. Why does every equality now pass (F3.2)?

Check Yourself

module sec_dbg(input clk, rst, start, key_ld, input [7:0] din, key_in, input [1:0] dbg_sel,
  output [7:0] dout, output reg [7:0] dbg=0);
  reg [7:0] key=0, acc=0;
  reg [3:0] cnt=0;
  reg busy=0;
  wire [7:0] mix = acc ^ key;
  assign dout = (mix << cnt[2:0]) | (mix >> (4'd8 - cnt[2:0]));   // the ciphertext: may depend on key
  always @(posedge clk)
    if (rst) begin key <= 0; acc <= 0; cnt <= 0; busy <= 0; dbg <= 0; end
    else begin
      if (key_ld) key <= key_in;
      if (start) begin busy <= 1; cnt <= 0; acc <= din; end
      else if (busy) begin cnt <= cnt + 4'd1; acc <= acc + din; if (cnt == 4'd7) busy <= 0; end
      case (dbg_sel)                                   // the debug port: must not depend on key
        2'd0: dbg <= {4'd0, cnt};
        2'd1: dbg <= {busy, 3'd0, cnt};
        2'd2: dbg <= {7'd0, key[0]};   // bug: a shifted bus lands key[0] here
        2'd3: dbg <= acc;
      endcase
    end
endmodule

// Self-composition: two copies, every public input shared, only the secret differs.
module sec_top(input clk, rst, start, key_ld, input [7:0] din, input [1:0] dbg_sel);
  (* anyconst *) reg [7:0] k_a, k_b;   // two secrets, chosen once by the solver
  wire [7:0] dout_a, dout_b, dbg_a, dbg_b;
  sec_dbg a(.clk(clk), .rst(rst), .start(start), .key_ld(key_ld), .din(din), .key_in(k_a), .dbg_sel(dbg_sel), .dout(dout_a), .dbg(dbg_a));
  sec_dbg b(.clk(clk), .rst(rst), .start(start), .key_ld(key_ld), .din(din), .key_in(k_b), .dbg_sel(dbg_sel), .dout(dout_b), .dbg(dbg_b));
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  always @(posedge clk) if (!rst) begin
    assert(dbg_a == dbg_b);   // the sink must not see the secret
  end
`endif
endmodule