Prove it once. Reuse the evidence.

Reusable verified security component

Prove your security component once. Reuse the evidence in every product.

Isolation, access control, protocol state and message integrity. We formally model the property, a theorem prover checks that your component meets it, and we adapt that evidence for each product built on the component.

Discuss your component

Why prove per component

Under CC:2022, a formal security policy model (ADV_SPM.1) normally has to cover all of a product's security functionality. For a complex product, that model is expensive to build, prove and evaluate.

ENISA's EUCC guidance on the transition to CC:2022 shows the direction of travel: formal evidence for well-defined parts of the security functionality, such as memory management and code loading on security ICs, and the application firewall on Java Card platforms. The certificate then states both the assurance level of the whole product and the level reached by the modelled parts.

A component used across a product line is the natural unit to prove. Model and prove it once, then carry the evidence into every product built on it.

Read ENISA's guidance on formal methods in the CC:2022 transition (opens in a new tab)

What we prove

Isolation

One application or partition cannot read or write memory that belongs to another.

Typical targets: MPU and MMU configuration, partitions, separation kernels

Access control

Every access is checked against the policy, and no path through the component bypasses the check.

Typical targets: Application firewalls, permission models, key usage rules

Protocol state

The component never skips authentication and never accepts a message out of order.

Typical targets: Secure channels, code loaders, lifecycle states

Message integrity

Nothing is accepted unless its integrity check passes, and parsing accepts exactly the specified format.

Typical targets: Signed code images, commands, message parsers

Prove once, reuse the evidence

  1. Specify

    We agree the security properties and a formal model of the component with your engineers. The specification is what people review.

  2. Prove

    AI proposes the proofs. A theorem prover checks every step, and every assumption is written down.

  3. Bind

    The proofs are tied to the exact component version by digest, and re-run whenever the component changes.

  4. Adapt

    For each product that uses the component, we map the proven properties to the security objectives and security functional requirements in its Security Target.

What you receive

  • A formal security policy model of the component
  • Machine-checked proofs of the agreed security properties
  • A written list of assumptions, each recording how it is established and how it could become invalid
  • The correspondence between the model and the functional specification
  • A mapping to each product's Security Target
  • Proof scripts you can re-run whenever the component changes

Your evaluation lab evaluates each product and your certification body certifies it. We provide the formal evidence they assess.

Who it is for

Smart card, secure element and Java Card vendors

  • MPU and MMU memory management
  • Code loading
  • The Java Card application firewall
  • Platforms shared across many certified products

Suppliers of other reusable components

  • Separation kernels and hypervisors
  • Secure boot and code loaders
  • Cryptographic libraries
  • Protocol stacks and secure channels

Built on vericoding

Vericoding is our method. People write and review the specification, AI proposes the implementation and the proof, and a theorem prover checks the result. Our experiments show it at work on protocols and parsers: SpecAMQP, an open Lean specification of the AMQP 1.0 protocol, and parsebot, a JSON parser proved against its grammar in Rocq. They are research results, not security certifications.

Discuss your component

Tell us the component, the Protection Profile and the assurance level you are aiming for.

Send us a message