code wiki / _hdl_build / nx_evattest_gate.nx
`nx_evattest_gate.nx` source

↩ module page · 221 lines · 11691 B
1// nx_evattest_gate.nx -- proves the signed-attestation layer accepts a genuine operator sign-off and
2// REFUSES every way of faking one. The clause it defends (`require_human`) is the single thing standing
3// between "an agent certified its own work" and a PROVEN verdict, so every refusal path here is
4// negative-controlled: a gate that only ever demonstrates acceptance has proven nothing.
5// license_tier: ORIGINAL  expect_exit: 0
6import "nx_syscalls.nx"
7import "nx_evattest.nx"
8
9func w(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 }
10func wn(v: i64) -> i64 { let t: *u8=sys_mmap(28); var m: i64=v; var k: i64=0; if m==0{t[0]=48 as u8;k=1} while m>0{t[k]=(48+(m%10)) as u8;m=m/10;k=k+1} let b: *u8=sys_mmap(28); var i: i64=0; while i<k{b[i]=t[k-1-i];i=i+1} sys_write(1,b,k); return 0 }
11func ck(pass: i64, label: *u8, fails: *i64) -> i64 {
  w("  " as *u8); w(label); w(": " as *u8)
  if pass==1 { w("PASS\n" as *u8) } else { w("FAIL\n" as *u8); fails[0]=fails[0]+1 }
  return 0
15}
16func hexout(src: *u8, n: i64, dst: *u8, off: i64) -> i64 {
  let hexd: *u8 = "0123456789abcdef"
  var o: i64 = off
  var i: i64 = 0
  while i < n {
      let b: i64 = src[i] as i64
      dst[o] = hexd[(b >> 4) & 15]; o = o + 1
      dst[o] = hexd[b & 15]; o = o + 1
      i = i + 1
  }
  return o
27}
28func cat(dst: *u8, off: i64, s: *u8) -> i64 {
  var o: i64 = off
  var i: i64 = 0
  while s[i] != (0 as u8) { dst[o] = s[i]; o = o + 1; i = i + 1 }
  return o
33}
34
35func main() -> i64 {
  let fails: *i64 = sys_mmap(16) as *i64
  fails[0]=0
  w("=== nx_evattest_gate -- a genuine operator sign-off passes; every forgery is refused ===\n" as *u8)
39
  // Two deterministic test keys. HUMAN = the operator's; MACHINE = one the automation might hold.
  let hpriv: *u8 = sys_mmap(32)
  let mpriv: *u8 = sys_mmap(32)
  var i: i64 = 0
  while i < 32 { hpriv[i] = (i + 11) as u8; mpriv[i] = (i + 200) as u8; i = i + 1 }
  let hpub: *u8 = sys_mmap(32)
  let mpub: *u8 = sys_mmap(32)
  ed25519_pub_from_priv(hpriv, hpub)
  ed25519_pub_from_priv(mpriv, mpub)
49
  // Key registry: the human key is role=human, the machine key role=machine. A third key is left
  // deliberately unregistered so "valid signature from a stranger" can be tested.
  let conf: *u8 = sys_mmap(4096)
  var c: i64 = 0
  c = cat(conf, c, "# test registry\nrole=human pub=" as *u8)
  c = hexout(hpub, 32, conf, c)
  c = cat(conf, c, " name=operator\nrole=machine pub=" as *u8)
  c = hexout(mpub, 32, conf, c)
  c = cat(conf, c, " name=automation\n" as *u8)
59
  // ---- build a genuine human attestation ----
  let row: *u8 = sys_mmap(4096)
  var r: i64 = 0
  r = cat(row, r, "class=human verdict=pass scope=reviewed-9-warden-axes-against-source signer=operator epoch=1785400000" as *u8)
  let sig: *u8 = sys_mmap(64)
  ed25519_sign_full(hpriv, row, r, sig)
  var rf: i64 = cat(row, r, " pub=" as *u8)
  rf = hexout(hpub, 32, row, rf)
  rf = cat(row, rf, " sig=" as *u8)
  rf = hexout(sig, 64, row, rf)
70
  // T1: the genuine operator attestation is ACCEPTED (the layer is usable, not merely strict)
  var t1: i64=0
  if at_verify_row(row, 0, rf, AT_CLASS_HUMAN, conf, c)==AT_OK { t1=1 }
  ck(t1, "T1 genuine operator-signed human row -> OK (accepts real sign-off)" as *u8, fails)
75
  // T2: THE ATTACK THIS EXISTS TO STOP -- the automation signs a human-class row with ITS OWN key.
  // Cryptographically valid, registered key, and still REFUSED on role.
  let row2: *u8 = sys_mmap(4096)
  var r2: i64 = 0
  r2 = cat(row2, r2, "class=human verdict=pass scope=I-checked-my-own-work signer=automation epoch=1785400000" as *u8)
  let sig2: *u8 = sys_mmap(64)
  ed25519_sign_full(mpriv, row2, r2, sig2)
  var rf2: i64 = cat(row2, r2, " pub=" as *u8)
  rf2 = hexout(mpub, 32, row2, rf2)
  rf2 = cat(row2, rf2, " sig=" as *u8)
  rf2 = hexout(sig2, 64, row2, rf2)
  var t2: i64=0
  if at_verify_row(row2, 0, rf2, AT_CLASS_HUMAN, conf, c)==AT_ERR_ROLE { t2=1 }
  ck(t2, "T2 MACHINE key signs a human row (valid sig, registered) -> REFUSED on role" as *u8, fails)
90
  // T3: the same machine key IS accepted for a machine-class claim -- role separation is a boundary,
  // not a blanket refusal of the automation.
  var t3: i64=0
  if at_verify_row(row2, 0, rf2, AT_CLASS_MECH, conf, c)==AT_OK { t3=1 }
  ck(t3, "T3 same machine key for a MECH claim -> OK (separation, not blanket refusal)" as *u8, fails)
96
  // T4: TAMPER -- flip one byte of the signed scope. Signature must fail.
  let row3: *u8 = sys_mmap(4096)
  var q: i64 = 0
  while q < rf { row3[q] = row[q]; q = q + 1 }
  row3[30] = (row3[30] as i64 + 1) as u8
  var t4: i64=0
  if at_verify_row(row3, 0, rf, AT_CLASS_HUMAN, conf, c)==AT_ERR_BADSIG { t4=1 }
  ck(t4, "T4 one byte of the signed scope altered -> BAD-SIGNATURE (tamper-evident)" as *u8, fails)
105
  // T5: an UNSIGNED row -- the pre-seq1367 format -- must not be honoured at all.
  let row4: *u8 = sys_mmap(1024)
  let r4: i64 = cat(row4, 0, "class=human verdict=pass scope=trust-me signer=whoever epoch=1785400000" as *u8)
  var t5: i64=0
  if at_verify_row(row4, 0, r4, AT_CLASS_HUMAN, conf, c)==AT_ERR_NOSIG { t5=1 }
  ck(t5, "T5 legacy UNSIGNED row -> UNSIGNED (fails closed, not grandfathered)" as *u8, fails)
112
  // T6: a VALID signature from an UNREGISTERED key is still refused -- a signature from a stranger is
  // not an authorisation.
  let upriv: *u8 = sys_mmap(32)
  i = 0
  while i < 32 { upriv[i] = (i + 77) as u8; i = i + 1 }
  let upub: *u8 = sys_mmap(32)
  ed25519_pub_from_priv(upriv, upub)
  let row5: *u8 = sys_mmap(4096)
  var r5: i64 = 0
  r5 = cat(row5, r5, "class=human verdict=pass scope=stranger-signed signer=nobody epoch=1785400000" as *u8)
  let sig5: *u8 = sys_mmap(64)
  ed25519_sign_full(upriv, row5, r5, sig5)
  var rf5: i64 = cat(row5, r5, " pub=" as *u8)
  rf5 = hexout(upub, 32, row5, rf5)
  rf5 = cat(row5, rf5, " sig=" as *u8)
  rf5 = hexout(sig5, 64, row5, rf5)
  var t6: i64=0
  if at_verify_row(row5, 0, rf5, AT_CLASS_HUMAN, conf, c)==AT_ERR_UNKNOWNKEY { t6=1 }
  ck(t6, "T6 valid signature from an UNREGISTERED key -> refused (a signature is not an authorisation)" as *u8, fails)
132
  // T7: SIGNATURE-SWAP -- take the genuine human signature and paste it onto a different claim.
  // The canonical message covers class/verdict/scope/epoch, so a lifted signature cannot be re-pointed.
  let row6: *u8 = sys_mmap(4096)
  var r6: i64 = 0
  r6 = cat(row6, r6, "class=human verdict=pass scope=SOMETHING-ELSE-ENTIRELY signer=operator epoch=1785400000" as *u8)
  var rf6: i64 = cat(row6, r6, " pub=" as *u8)
  rf6 = hexout(hpub, 32, row6, rf6)
  rf6 = cat(row6, rf6, " sig=" as *u8)
  rf6 = hexout(sig, 64, row6, rf6)
  var t7: i64=0
  if at_verify_row(row6, 0, rf6, AT_CLASS_HUMAN, conf, c)==AT_ERR_BADSIG { t7=1 }
  ck(t7, "T7 genuine signature lifted onto a DIFFERENT claim -> BAD-SIGNATURE (cannot be re-pointed)" as *u8, fails)
145
  // ---- T8..T12: THE ORACLE CLASS -- DERIVED, NEVER DECLARED (added 2026-07-31 with AT_CLASS_ORACLE) ----
  // Before this, EV_CLASS_ORACLE(8) reached at_verify_row and matched NO rule, so it was authorised by
  // fall-through and no tooth here could tell. A clause with no negative control has not been shown to
  // measure anything -- so each of the three required fields gets its own failing case.
  // The signature is REAL and the key is REGISTERED in every one of these rows: the only thing under test
  // is whether the CLAIM carries its own re-derivation recipe. That isolation is the point -- it proves
  // the refusal is about verifiability, not about the signer.
  let ro: *u8 = sys_mmap(4096)
  var q0: i64 = 0
  q0 = cat(ro, q0, "class=oracle verdict=pass scope=sha256-native ref=FIPS 180-4 refdig=d719137726632612 gate=nx_sha256_native_kat_gate signer=automation epoch=1785400000" as *u8)
  let sigo: *u8 = sys_mmap(64)
  ed25519_sign_full(mpriv, ro, q0, sigo)
  var rfo: i64 = cat(ro, q0, " pub=" as *u8)
  rfo = hexout(mpub, 32, ro, rfo)
  rfo = cat(ro, rfo, " sig=" as *u8)
  rfo = hexout(sigo, 64, ro, rfo)
  var t8: i64=0
  if at_verify_row(ro, 0, rfo, AT_CLASS_ORACLE, conf, c)==AT_OK { t8=1 }
  ck(t8, "T8  complete oracle row, MACHINE key -> OK (independence is in the REFERENCE, not the signer)" as *u8, fails)
165
  // T9 NEG: drop refdig=. This is the field that makes the class ungameable -- prose can claim FIPS 180-4,
  // only a digest commits to the bytes that were actually compared.
  let r9: *u8 = sys_mmap(4096)
  var q9: i64 = 0
  q9 = cat(r9, q9, "class=oracle verdict=pass scope=sha256-native ref=FIPS 180-4 gate=nx_sha256_native_kat_gate signer=automation epoch=1785400000" as *u8)
  let sig9: *u8 = sys_mmap(64)
  ed25519_sign_full(mpriv, r9, q9, sig9)
  var rf9: i64 = cat(r9, q9, " pub=" as *u8)
  rf9 = hexout(mpub, 32, r9, rf9)
  rf9 = cat(r9, rf9, " sig=" as *u8)
  rf9 = hexout(sig9, 64, r9, rf9)
  var t9: i64=0
  if at_verify_row(r9, 0, rf9, AT_CLASS_ORACLE, conf, c)==AT_ERR_NOTDERIVED { t9=1 }
  ck(t9, "T9  NEG oracle row without refdig= -> NOT-DERIVED (a claim that commits to no bytes)" as *u8, fails)
180
  // T10 NEG: drop gate=. Without the recipe the reader cannot re-run the comparison, and re-runnability
  // is the whole reason this class does not need to be trusted.
  let r10: *u8 = sys_mmap(4096)
  var q10: i64 = 0
  q10 = cat(r10, q10, "class=oracle verdict=pass scope=sha256-native ref=FIPS 180-4 refdig=d719137726632612 signer=automation epoch=1785400000" as *u8)
  let sig10: *u8 = sys_mmap(64)
  ed25519_sign_full(mpriv, r10, q10, sig10)
  var rf10: i64 = cat(r10, q10, " pub=" as *u8)
  rf10 = hexout(mpub, 32, r10, rf10)
  rf10 = cat(r10, rf10, " sig=" as *u8)
  rf10 = hexout(sig10, 64, r10, rf10)
  var t10: i64=0
  if at_verify_row(r10, 0, rf10, AT_CLASS_ORACLE, conf, c)==AT_ERR_NOTDERIVED { t10=1 }
  ck(t10, "T10 NEG oracle row without gate= -> NOT-DERIVED (no re-derivation recipe)" as *u8, fails)
195
  // T11 NEG: THE PROSE FORGERY. Drop ref= -- an oracle that will not say what it matched.
  let r11: *u8 = sys_mmap(4096)
  var q11: i64 = 0
  q11 = cat(r11, q11, "class=oracle verdict=pass scope=sha256-native refdig=d719137726632612 gate=nx_sha256_native_kat_gate signer=automation epoch=1785400000" as *u8)
  let sig11: *u8 = sys_mmap(64)
  ed25519_sign_full(mpriv, r11, q11, sig11)
  var rf11: i64 = cat(r11, q11, " pub=" as *u8)
  rf11 = hexout(mpub, 32, r11, rf11)
  rf11 = cat(r11, rf11, " sig=" as *u8)
  rf11 = hexout(sig11, 64, r11, rf11)
  var t11: i64=0
  if at_verify_row(r11, 0, rf11, AT_CLASS_ORACLE, conf, c)==AT_ERR_NOTDERIVED { t11=1 }
  ck(t11, "T11 NEG oracle row without ref= -> NOT-DERIVED (it matched WHAT?)" as *u8, fails)
209
  // T12: the derived contract binds ONLY the oracle class. The same recipe-less row is fine as a MECH
  // claim -- so the new clause raised the bar for one class without silently tightening the others.
  var t12: i64=0
  if at_verify_row(r11, 0, rf11, AT_CLASS_MECH, conf, c)==AT_OK { t12=1 }
  ck(t12, "T12 same recipe-less row as a MECH claim -> OK (the clause is scoped, not a blanket)" as *u8, fails)
215
  w("  fails=" as *u8); wn(fails[0]); w("\n" as *u8)
  if fails[0]==0 { w("VERDICT: verdict=GREEN (signed attestations: real sign-off accepted; machine-signed human rows, tampering, lifting, strangers and legacy unsigned rows all refused)\n" as *u8); sys_exit(0) }
  w("VERDICT: verdict=RED\n" as *u8)
  sys_exit(1)
  return 1
221}
nx_evattest_gate.nx source

`nx_evattest_gate.nx` source
