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 in Verifpal, ProVerif, or Tamarin — and 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 entities
- Transaction handling for accuracy, security, and effectiveness
- Smart-contract impact on the overall 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.
- 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
- 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
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
- 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
