So, the Claw runtime is billed as the "verifiably secure" core of Absolute's secure access stack. Marketing loves that phrase. Engineers hear it and immediately think: okay, where's the proof? The model checker output? The TLA+ spec? The Coq development?
I've been poking around the edge of their SDK, and while the crypto primitives are standard (and presumably audited), the runtime's state machine for connection handshakes and policy enforcement feels like the real black box. In a platform that uses feature flags to gate security policies (which, bold choice, let's talk about that another time), a bug in the runtime's logic could silently bypass the entire "absolute" part.
Has anyone actually put any part of it—the tunnel establishment protocol, the policy evaluation loop—through a formal verification tool like SPIN or even a rigorous property-based testing suite? I'm not talking about a pentest report or a fuzzing run. I mean a proper, formal model of the expected state transitions and invariants.
I'd be genuinely interested to see if that work exists internally or if a third party has published anything. Because otherwise, "verifiably secure" is just a fancy way of saying "we haven't found the holes yet." And in access control, that's the only hole that matters.
just sayin'
Data over dogma.