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. We work above that layer: protocol architecture, cryptographic design, and threat models reviewed before the first line of code, then implementation fidelity checked against them afterwards. A senior cryptography expert leads every engagement.
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
We check whether the chosen primitives fit the threat model and whether they compose correctly, across AEAD, KDF, signature, and KEM.
Adversary capability assessment
We work out what the design assumed the adversary can do, and whether those assumptions are tight. AI bug-finders do not question threat models.
Cross-language code review
We read the full source in Go, Rust, TypeScript, Swift, Java, .NET, C, and Solidity, checking that the implementation matches the design.
PQ migration assessment
We assess whether your system survives the next decade of cryptanalytic advances: KEM hybridisation, signature strategy, library and protocol fitness.
Machine-checked proofs
Symbolic verification of protocol correctness in Verifpal, ProVerif, or Tamarin, plus critical review of formal-verification claims others have made about code you depend on.
When 'verified' isn't: critical analysis of a high-assurance library
Five findings across CE Labs' libcrux cryptographic library, marketed as formally verified. We documented structural gaps in Cryspen's hax verification pipeline that libcrux's proofs rely on, 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 Cryspen's hax verification pipeline
- ML-DSA conformance issues caught by Crucible
- Verification facade: proofs that didn't cover what the marketing claimed
- F-01runtimeML-KEM decompression: 1664 where
pow2 (d−1)belongs - F-02proofSerialization proof claims bound 1; code allows 12
- F-03fipsML-DSA verifier norm check missing (FIPS 204)
- F-04fipsHint deserialization accepts malformed hints
- F-05proofAVX2 axiom models x·x where hardware does x·y
Telegram's MTProto: deanonymization potential for a network attacker
A technical review of Telegram's MTProto protocol under a network-attacker threat model, commissioned in 2025 by Global Network Solutions and made public in 2026 through a Swiss court filing. Conducted under editorial-independence terms reproduced verbatim in the report.
- 64-bit
auth_key_idexposed in cleartext on every message, on every platform tested - Telegram Desktop uses port 443 without TLS, verified four independent ways
- Identifier persists across app restarts, IP changes, and network switches
- Full editorial control retained by Symbolic Software, per Section 2.4 of the report
- F-01crit
auth_key_idin cleartext on every message - F-02highTelegram Desktop: port 443, without TLS
- F-03medIdentifier survives restarts, IP & network changes
- §2.4noteFull editorial independence, reproduced verbatim
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
- S-01✓Threshold correctness across the signing flow
- S-02✓Ceremony robustness, partially-malicious parties
- S-03✓Primitive use and composition
- S-04✓Rust-specific implementation hardening
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 systems
- Transaction handling, checked for correctness and security
- Smart-contract effects on the user experience
- S-01✓Gas efficiency at the design level
- S-02✓On-chain and off-chain transaction flows
- S-03✓Liquidity models and scalability
- F-02medCold-storage gas spike in transfer path
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.
- Confirmed that 1Password's key-management architecture holds up
- Showed how much vault security depends on key rotation
- Found vulnerabilities that appear when the server is compromised
- Recommended stricter public-key validation
- F-01highVault exposure under server compromise
- F-02medPublic-key validation needs hardening
- S-03✓Key-rotation architecture affirmed
- S-04✓Key-management design robust
PGP signature path & envelope integrity
Our first 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 when combined with social engineering
- Identified how message confidentiality could be lost
- F-01critCritical flaw in Enigmail’s signature path
- F-02highEncrypted mail exposed to attacker mutation
- F-03medExploitation path via social engineering
- —noteThe founding engagement of the practice
