Protocol design review
Key exchange, authentication flows, session management, state machines. We evaluate the architecture before the first line of implementation code.
Security auditing
for the AI era.
AI systems can now find and exploit implementation bugs at scale. The audits that matter go deeper: evaluating protocol architecture, cryptographic design, and threat models before the first line of code, and verifying implementation fidelity afterwards. Each engagement led by a senior cryptography expert, not a junior analyst running a scanner.
ID
Severity
Title
- F-001 CRIT Authentication bypass via legacy-mode downgrade
- F-002 HIGH AEAD nonce uniqueness not preserved under concurrency
- F-003 HIGH Public key not validated to correct subgroup
- F-004 HIGH Padding oracle in legacy CBC fallback path
- F-005 MED Constant-time leak in ECC scalar multiplication
- F-006 MED Domain separation tag collision risk in KDF
- F-007 MED Replay window unbounded under burst conditions
- ⋮ + 5 more findings
⊕ 12 findings · 1 critical · 3 high · 5 medium · 3 informational
Security services
Primitive selection & composition
Are the chosen primitives appropriate for the threat model? Do they compose correctly? AEAD, KDF, signature, KEM — every choice scrutinized.
Adversary capability assessment
What did the design assume the adversary can do? Are those assumptions tight? AI bug-finders cannot challenge threat models — humans must.
Cross-language code review
Does the code correctly realize the design? Go, Rust, TypeScript, Swift, Java, .NET, C, Solidity. Full-source audits, not scanner reports.
PQ migration assessment
Is your system positioned to survive the next decade of cryptanalytic advances? KEM hybridisation, signature strategy, library and protocol fitness.
Machine-checked proofs
Symbolic verification of protocol correctness, using the most appropriate tool for your target.
When 'verified' isn't: critical analysis of a high-assurance library
Five findings across Cryspen's libcrux cryptographic library, marketed as formally verified. We documented structural gaps in their hax verification pipeline, ML-DSA implementation issues, and limitations in their TLS approach. Two papers and an OSTIF talk followed.
- 5 distinct bug findings across libcrux's verified-marketed code
- Structural gaps in the hax verification pipeline
- ML-DSA conformance issues caught by Crucible
- Verification facade: proofs that didn't cover what the marketing claimed
theoremaead_correct⊢✓
theoremaead_authentic⊢✓
theoremnonce_unique⊢✓
theorempadding_safe⊢✓
theoremkdf_separation⊢✗ stuck
└─ missing: ¬collision on HKDF info
4/5 verified · spec gap · "verified" facade
2PC-MPC threshold signature audit, in Rust
We reviewed the dWallet Labs 2PC-MPC threshold-signature implementation in Rust. The audit covered MPC ceremony correctness, secret-sharing validity, primitive composition, and side-channel exposure across the signing protocol.
- Threshold protocol correctness across the full signing flow
- MPC ceremony robustness under partially-malicious participants
- Cryptographic primitive use and composition
- Rust-specific implementation hardening
[r1]commitP₁ P₂ P₃ P₄ P₅
[r2]openP₁ P₂ P₄⌛ t=3 ✓
[r3]σᵢfragments collected from S
[r4]σ = lagrange(S)
✓σ = 0x7a3b9c01…e8f2
Smart contract architecture audit
We evaluated the Native Labs smart contracts across performance, security, interoperability, on-chain and off-chain transaction flows, liquidity models, and user experience. Special attention to gas efficiency at the design level.
- Operational efficiency, with emphasis on gas, scalability, and transaction speed
- Integration with internal and third-party entities
- Transaction handling for accuracy, security, and effectiveness
- Smart-contract impact on the overall user experience
[op 01]tx.origin check21,000
[op 02]sload (warm)+ 2,100
[op 03]call.value+ 9,000
[op 04]sstore (cold)+22,100⚠
[op 05]keccak256+ 72
↑54,272 gas · cold-storage spike (F-002)
Password manager B5 architecture & key rotation
Pentest of 1Password B5, conducted in collaboration with Cure53. Our contribution focused on key rotation correctness, vault security under server compromise, and public-key validation hardening.
- Affirmed the robustness of 1Password's key-management architecture
- Highlighted the critical role of key rotation for vault security
- Identified vulnerabilities under server-compromise scenarios
- Stressed the need for robust public-key validation
unlockmk ← argon2id(password, salt)
derivevk ← hkdf(mk, "vault")
rotate∀ item ∈ vault: Ek₁(Dk₀(item))
attestσ ← sign(sk, rotation_proof)
publishk₁ → server (E2E sealed)
✓1,247 items re-encrypted · 0 leaks
PGP signature path & envelope integrity
Symbolic Software's foundational client engagement. Working with Cure53, we audited Mozilla Thunderbird's Enigmail PGP integration, identifying a critical vulnerability that exposed encrypted messages to a class of attacker-mutation attacks.
- Detected a critical vulnerability in Enigmail's signature path
- Outlined exposure of encrypted messages to attacker mutation
- Evaluated exploitation risk combined with social engineering
- Identified potential confidentiality compromise
─BEGIN PGP SIGNED MESSAGE─
Hash:SHA512[body 248 B]
─BEGIN PGP SIGNATURE─
verifyed25519(pk, sha512(body), σ)
└─ pk =4b7e d8a2 1f3c …
└─ h =a3f5 9c01 …← mutated
✗signature mismatch · in-flight tampering
Ready to secure your architecture?
AI is changing what attackers can do. We help you change what they find.
Secure your architecture →