Security: Our Core

KeyHippo uses TLA+ (Temporal Logic of Actions) to mathematically verify our core systems. Here are some of the critical properties we're working to verify:

• Token Validity: We're developing a TLA+ specification to ensure that for all tokens t in the set of active tokens, if the current time is less than the token's expiration time, then VerifyJWT(t) must hold true.
• Revocation Effectiveness: Our model aims to prove that for any token t in the set of revoked tokens, VerifyJWT(t) is always false, guaranteeing that revoked tokens can never be used.
• Usage Limit Enforcement: We're working on verifying that for all tokens t, the number of times t has been used is always less than or equal to the maximum allowed uses (e.g., TokenUses[t] <= MaxTokenUses).
• Temporal Consistency: Our specification is being designed to prove that the issuance time (iat) of any token is always less than or equal to the current system time, and the expiration time (exp) is always greater than the issuance time.
• User Token Limit: We're developing verification processes to ensure that for all users u, the number of active tokens associated with u never exceeds the maximum allowed tokens per user.

Our API key system is built on a foundation of cryptographic irreversibility. We leverage multi-stage hashing processes and high-precision timestamps to ensure each key is unique and impossible to reconstruct, even with full database access.

• Zero Knowledge Storage: API keys are never stored in any form. We maintain only cryptographically hashed references.
• Temporal Uniqueness: Nanosecond-precision timestamps ensure uniqueness even for keys generated in rapid succession.
• Multi-Layer Encryption: We employ a series of HMAC operations with SHA-512, using secrets stored in Supabase Vault for enhanced security.
• Breach Resilience: In the unlikely event of a database compromise, the stored hashes provide no mechanism to regenerate or deduce the original API keys.

Our authentication process seamlessly integrates with Supabase's Row Level Security (RLS) framework, providing a unified security model across session-based and API key authentication methods.

• Key Extraction and Hashing: On each request, the API key is extracted and immediately hashed using our secure multi-stage process.
• Vault-Based Verification: The hashed key is verified against references stored in Supabase Vault, never touching the main database.
• RLS Integration: Once authenticated, the request is seamlessly integrated into existing RLS policies, maintaining granular access control.
• Real-time Policy Enforcement: All RLS policies are evaluated in real-time, incorporating both the authenticated user ID and key-specific validations.

Our approach to security is proactive and iterative. We maintain a robust incident response plan and continuously refine our systems to stay ahead of emerging threats.

In the event of a security incident, our team is prepared to respond swiftly, implementing containment measures and conducting thorough post-incident analysis to prevent future occurrences.

Security is ingrained in our development process from the ground up. We adhere to strict coding standards and employ automated security checks at every stage of our CI/CD pipeline.

• Code Analysis: We use static and dynamic code analysis tools to identify potential vulnerabilities before they reach production.
• Dependency Scanning: Our automated systems continuously monitor and update dependencies to mitigate potential supply chain attacks.

We value the insights of the security community. If you've identified a potential vulnerability, please contact us immediately at hello@integrated-reasoning.com. We're committed to rapid response and resolution of all reported issues.

Have questions about our security architecture or practices? We're always available to discuss the technical details of how we're protecting your data. Reach out to us at hello@integrated-reasoning.com.