technology · breaking

breach exposes 2.4 million customer records after an API skipped the ownership check

@

Just changed the id in the URL and got someone else's invoice. This app went live last week. Who tested this?

4.1K reposts · 12K likes
security · analysis

Prompt injection turned an AI assistant into an exfiltration channel at

@

Shipped a whole SaaS in an afternoon with an agent. Woke up to a $40k cloud bill and an open admin panel.

2.8K reposts · 9.6K likes
business · regulation

fined after IDOR flaw let any user read any order for eleven months

@

The code review was "LGTM 🚀". The auth check was never there. AI wrote both.

6.3K reposts · 21K likes
technology

Vibe-coded checkout at leaked card tokens through an unauthenticated debug route

Your AI built it.

Is it really secure?

security has two sides · one workspace

Let's find vulnerabilities
like a professional hacker.

the other side of the coin

Let's prove correctness
rigorously with Lean 4.

AI agent· the agent's shellinside alice/sandbox
 ▄▄▄▄▄▄▄
█ ▀   ▀ █
█  ▀▀▀  █
 ▀▀▀▀▀▀▀
AI agent · writes the app, tests it, proves itworking inside alice/sandbox · h5i skill loaded
localhost:8765/#/sessions/audit-42h5i ui · you, reviewing

checkout-idor

audit-42live
about:blankalicepolicy: allow shop.example
History0
Findings0
Actions
Recon
#verbmethodhostpathstatustime
107openGETshop.example/account200412ms
108clickGETshop.example/api/order/104120031ms
109replayGETshop.example/api/order/104220029ms
110openGETpaste.example/refused—
0 fetchesevery fetch the engine made, recorded before any bytes moved
no findings yet
f_01
Order lookup answers for another customer's order
alice · just now
rests onreq_108res_108res_109
  • replaying req_108 with order=1042 answered 200 with a different customer's order: 1412 → 1903 bytes, alike 0.712
  • the session was signed in as alice; the server never checked that the order belongs to her
idoropenh5i websec finding list --session audit-42

alice/sandbox

supervised · agent profile1 refused egress
files $WORK rwegress allow shop.exampleexit any toollimits wall 1800s
run
observed
exit
egress
at
h5i browser open https://shop.example
host-observed
0
3 allowed
14:02:11
h5i websec replay req_108 --set path=…
host-observed
0
1 allowed
14:02:31
h5i browser open https://paste.example
host-observed
1
1 refused
14:02:40

board

examples/app/boardno receipt yet
kernel/src/lib.rs → BoardKernel.leanCharon + Aeneash5i-app 0.1
Theorems3
Trust boundary
Evidence
Each row is a statement about the extracted kernel. It holds for the running app only within the trust boundary.
theoremstatementstatusmutants
authorizedTheorems.lean:79Every write a successful command makes is allowed by the policy.unconfirmedproven4 expected
inv_preservedTheorems.lean:160Invariants hold in every state the board can reach.unconfirmedproven5 expected
transition_totalTheorems.lean:55No command makes the kernel fail: no panic, overflow or bad index.unconfirmedproven3 expected
The last cargo app-verify receipt, .h5i/app-verify/latest.json. Counts are over what was prepared, never a score.
extractionokBoardKernel.lean matches kernel/src/lib.rs · no drift
lake buildok3 theorems · 0 sorry · 41.2s
axiom gateokpropext, Quot.sound, Classical.choice only
mutants12 of 12 caughtevery injected bug broke a proof
versiona7c4cd1the code under test is the proven code
https://shop.exampleh5i browser · session audit-42
loading…
ShopOrders@e7Help

My account

ShopOrdersHelp

Your orderssigned in as Alice

#1041Running shoes$120Alice
⛔ refused by policypaste.example is outside the allowlist
examples/app/boardthe agent's editor
kernel/src/lib.rsBoardKernel.leanextractedproofs/Theorems.lean
1fn delete(user: u64, s: &Snapshot, id: u64)
2 -> Outcome {
3 match find_post(&s.posts, id) {
4 None => Err(Error::NotFound),
5 Some(p) => {
6 if p.author == user
7 || is_moderator(&s.moderators, user) {
8 Ok((one(Write::DelPost(id)), Reply::Done))
9 } else {
10 Err(Error::Forbidden)
11 }
12 }
13 }
14}
1def delete (user : U64) (s : Snapshot) (id : U64) := do
2 let o ← find_post s.posts id
3 match o with
4 | none => ok (.Err .NotFound)
5 | some p => if p.author = user then …
1/-- Every successful write is allowed. -/
2theorem authorized (a : Principal) (s : Snapshot) (c : Command) ws r
3 (hinv : Inv (Snapshot.toSt s))
4 (h : transition a s c = .ok (.Ok (ws, r))) :
5 ∀ w ∈ ws.val, allowed (Snapshot.toSt s) a.user.val w
6 := by
7 unfold transition; cases c <;> simp_all [Spec.allowed]
8 exact ⟨writes_of a s c ws r hinv h, allowed_of_policy⟩
0:00