A debug register mirrors an internal key while the lock bit is off. Functionally everything passes: the mirror holds a value, reads return it, no protocol is violated. Only a proof that varies the secret sees the leak, because only it asks whether the observable outputs depend on what they must not. The symptom in the field is a key read out through a test interface nobody re-examined after tape-out, or a key still visible after the lock was set again.
Non-interference by two copies: instantiate the register-and-lock block twice with identical public inputs and the same unlock and re-lock commands, different secrets, and assert the public outputs agree whenever the block is locked. The claim is about the current state, not about history: after a legitimate unlock and a re-lock the outputs must again be independent of the secret, so a stale copy of the secret that survives the re-lock is a failure. A helper invariant says both copies are open or locked together, which is what makes the claim inductive. The leak variants route the secret to the output while locked, or keep a stale copy visible after a re-lock, and the copies visibly diverge. This proves value flow only: timing channels, power and any dependence through shared resources are outside the claim, and the lesson says so.
The lesson-local module below shows the secret on its output while the lock is open and the public input while it is locked. The two-copy harness compares the copies whenever the block is locked, and the proof passes. Three covers show the proof exercised the interesting cases: differing secrets while locked, the lock open, and differing secrets after a lock that had been open:
// formal: prove 4 expect pass slang top lock_top
`define FORMAL
module reg_lock #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire unlock,
input wire relock,
input wire [7:0] secret,
input wire [7:0] pub_in,
output wire [7:0] pub_out
);
reg opened; // the lock is open
reg [7:0] last; // a copy of the secret taken while the lock is open
always @(posedge clk) begin
if (rst) begin opened <= 1'b0; last <= 8'h00; end
else begin
if (unlock) opened <= 1'b1;
else if (relock) opened <= 1'b0;
if (opened) last <= secret;
end
end
// BUG 1: the secret reaches the output while locked. BUG 2: after a re-lock the stale copy is still mixed in.
assign pub_out = (BUG == 1) ? secret :
opened ? secret :
(BUG == 2) ? (pub_in ^ last) : pub_in;
endmodule
module lock_top #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire unlock,
input wire relock,
input wire [7:0] secret_a,
input wire [7:0] secret_b,
input wire [7:0] pub_in,
output wire [7:0] out_a,
output wire [7:0] out_b
);
reg_lock #(.BUG(BUG)) u_a (.clk(clk), .rst(rst), .unlock(unlock), .relock(relock),
.secret(secret_a), .pub_in(pub_in), .pub_out(out_a));
reg_lock #(.BUG(BUG)) u_b (.clk(clk), .rst(rst), .unlock(unlock), .relock(relock),
.secret(secret_b), .pub_in(pub_in), .pub_out(out_b));
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg seen_open;
always @(posedge clk) begin
if (rst) seen_open <= 1'b0;
else if (u_a.opened) seen_open <= 1'b1;
end
always @(*) if (!init) begin
h_open_equal: assert (u_a.opened == u_b.opened); // both copies are locked or open together
s_locked_equal: assert (u_a.opened || out_a == out_b); // locked now: the outputs cannot depend on the secret
c_locked_diff: cover (!u_a.opened && secret_a != secret_b);
c_unlocked: cover (u_a.opened);
c_relocked: cover (!u_a.opened && seen_open && secret_a != secret_b);
end
`endif
endmodule// formal: cover 8 expect reached slang top lock_top
`define FORMAL
module reg_lock #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire unlock,
input wire relock,
input wire [7:0] secret,
input wire [7:0] pub_in,
output wire [7:0] pub_out
);
reg opened; // the lock is open
reg [7:0] last; // a copy of the secret taken while the lock is open
always @(posedge clk) begin
if (rst) begin opened <= 1'b0; last <= 8'h00; end
else begin
if (unlock) opened <= 1'b1;
else if (relock) opened <= 1'b0;
if (opened) last <= secret;
end
end
// BUG 1: the secret reaches the output while locked. BUG 2: after a re-lock the stale copy is still mixed in.
assign pub_out = (BUG == 1) ? secret :
opened ? secret :
(BUG == 2) ? (pub_in ^ last) : pub_in;
endmodule
module lock_top #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire unlock,
input wire relock,
input wire [7:0] secret_a,
input wire [7:0] secret_b,
input wire [7:0] pub_in,
output wire [7:0] out_a,
output wire [7:0] out_b
);
reg_lock #(.BUG(BUG)) u_a (.clk(clk), .rst(rst), .unlock(unlock), .relock(relock),
.secret(secret_a), .pub_in(pub_in), .pub_out(out_a));
reg_lock #(.BUG(BUG)) u_b (.clk(clk), .rst(rst), .unlock(unlock), .relock(relock),
.secret(secret_b), .pub_in(pub_in), .pub_out(out_b));
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg seen_open;
always @(posedge clk) begin
if (rst) seen_open <= 1'b0;
else if (u_a.opened) seen_open <= 1'b1;
end
always @(*) if (!init) begin
h_open_equal: assert (u_a.opened == u_b.opened); // both copies are locked or open together
s_locked_equal: assert (u_a.opened || out_a == out_b); // locked now: the outputs cannot depend on the secret
c_locked_diff: cover (!u_a.opened && secret_a != secret_b);
c_unlocked: cover (u_a.opened);
c_relocked: cover (!u_a.opened && seen_open && secret_a != secret_b);
end
`endif
endmoduleThe first partner leaks the secret while locked. The copies diverge at the first checked step with differing secrets, and the same-state helper holds:
Step | lock | secret A / B |
| Outcome |
|---|---|---|---|---|
0 | locked | arbitrary | - | reset cycle, not checked |
1 | locked | differ | differ | leak variant: counterexample, |
1 | locked | differ | equal | correct variant: covered, still equal |
// formal: bmc 4 expect fail slang top lock_top define BUG=1
`define FORMAL
module reg_lock #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire unlock,
input wire relock,
input wire [7:0] secret,
input wire [7:0] pub_in,
output wire [7:0] pub_out
);
reg opened; // the lock is open
reg [7:0] last; // a copy of the secret taken while the lock is open
always @(posedge clk) begin
if (rst) begin opened <= 1'b0; last <= 8'h00; end
else begin
if (unlock) opened <= 1'b1;
else if (relock) opened <= 1'b0;
if (opened) last <= secret;
end
end
// BUG 1: the secret reaches the output while locked. BUG 2: after a re-lock the stale copy is still mixed in.
assign pub_out = (BUG == 1) ? secret :
opened ? secret :
(BUG == 2) ? (pub_in ^ last) : pub_in;
endmodule
module lock_top #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire unlock,
input wire relock,
input wire [7:0] secret_a,
input wire [7:0] secret_b,
input wire [7:0] pub_in,
output wire [7:0] out_a,
output wire [7:0] out_b
);
reg_lock #(.BUG(BUG)) u_a (.clk(clk), .rst(rst), .unlock(unlock), .relock(relock),
.secret(secret_a), .pub_in(pub_in), .pub_out(out_a));
reg_lock #(.BUG(BUG)) u_b (.clk(clk), .rst(rst), .unlock(unlock), .relock(relock),
.secret(secret_b), .pub_in(pub_in), .pub_out(out_b));
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg seen_open;
always @(posedge clk) begin
if (rst) seen_open <= 1'b0;
else if (u_a.opened) seen_open <= 1'b1;
end
always @(*) if (!init) begin
h_open_equal: assert (u_a.opened == u_b.opened); // both copies are locked or open together
s_locked_equal: assert (u_a.opened || out_a == out_b); // locked now: the outputs cannot depend on the secret
c_locked_diff: cover (!u_a.opened && secret_a != secret_b);
c_unlocked: cover (u_a.opened);
c_relocked: cover (!u_a.opened && seen_open && secret_a != secret_b);
end
`endif
endmoduleRoot cause of the leak: the output mux ignores the lock. Fix the mux, not the comparison. The second partner is subtler and is why the claim is about the current state and not about a never-opened lock: the lock is opened, the block keeps a copy of the secret, the block is locked again, and the stale copy is still mixed into the output. A check that only covered a never-opened lock would pass this design. The covers matter as much as the assertion: c_relocked shows the proof reached a locked block after it had been open:
// formal: bmc 8 expect fail slang top lock_top define BUG=2
`define FORMAL
module reg_lock #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire unlock,
input wire relock,
input wire [7:0] secret,
input wire [7:0] pub_in,
output wire [7:0] pub_out
);
reg opened; // the lock is open
reg [7:0] last; // a copy of the secret taken while the lock is open
always @(posedge clk) begin
if (rst) begin opened <= 1'b0; last <= 8'h00; end
else begin
if (unlock) opened <= 1'b1;
else if (relock) opened <= 1'b0;
if (opened) last <= secret;
end
end
// BUG 1: the secret reaches the output while locked. BUG 2: after a re-lock the stale copy is still mixed in.
assign pub_out = (BUG == 1) ? secret :
opened ? secret :
(BUG == 2) ? (pub_in ^ last) : pub_in;
endmodule
module lock_top #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire unlock,
input wire relock,
input wire [7:0] secret_a,
input wire [7:0] secret_b,
input wire [7:0] pub_in,
output wire [7:0] out_a,
output wire [7:0] out_b
);
reg_lock #(.BUG(BUG)) u_a (.clk(clk), .rst(rst), .unlock(unlock), .relock(relock),
.secret(secret_a), .pub_in(pub_in), .pub_out(out_a));
reg_lock #(.BUG(BUG)) u_b (.clk(clk), .rst(rst), .unlock(unlock), .relock(relock),
.secret(secret_b), .pub_in(pub_in), .pub_out(out_b));
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg seen_open;
always @(posedge clk) begin
if (rst) seen_open <= 1'b0;
else if (u_a.opened) seen_open <= 1'b1;
end
always @(*) if (!init) begin
h_open_equal: assert (u_a.opened == u_b.opened); // both copies are locked or open together
s_locked_equal: assert (u_a.opened || out_a == out_b); // locked now: the outputs cannot depend on the secret
c_locked_diff: cover (!u_a.opened && secret_a != secret_b);
c_unlocked: cover (u_a.opened);
c_relocked: cover (!u_a.opened && seen_open && secret_a != secret_b);
end
`endif
endmoduleThe comparison is conditioned on the block being locked now, not on it never having opened; the claim after a re-lock is stated and proved.
Both copies are shown to be in the same lock state by an invariant, not assumed.
All three covers are reachable: differing secrets while locked, the lock open, and differing secrets after a re-lock.
The claim states the limit: value flow through the named outputs, not timing, power or shared-resource channels.
A divergence with the lock open is legitimate traffic: check the lock state in the trace before calling it a leak. A divergence while locked names the path: walk the output expression for the secret and for any register that copied it. A proof that passes because the secrets never differ is vacuous: the differing-secrets covers are the guard.
Yes, through timing, and this proof cannot see it: non-interference here covers values on the named outputs only. Say so in the claim, and send the timing question to a dedicated channel analysis.