FYI:EC2’s formally verified “isolation engine” provides mathematical assurance of virtual-machine isolation
alex.shkotin
Alex
- The Nitro Isolation Engine is the core component of the Nitro Hypervisor, the first formally verified hypervisor deployed in a commercial cloud environment, ensuring correct behavior and enforcement of isolation between virtual machines.
- The formal verification of the Nitro Isolation Engine was achieved using the Isabelle/HOL proof assistant, resulting in 330,000 lines of machine-checked mathematics, comparable in scale to the seL4 project.
- The verification process involved creating a formalization of a core subset of the Rust language (μRust), using Separation Logic for specifications, and applying weakest-precondition calculus for proofs, all part of the open-sourced AutoCorrode library.
- The verification addressed four types of properties: confidentiality and integrity, functional correctness, absence of runtime errors, and memory safety, with confidentiality and integrity treated separately using noninterference and indistinguishability preservation.
- The Nitro Isolation Engine is designed for a commercial cloud environment and is an always-on feature for Graviton5 users, providing unprecedented visibility into how isolation is enforced.
alex.shkotin
John F Sowa
Alex Shkotin
John,
Sorry I forgot to link to the article:
It's interesting to compare the two languages, Isabelle/HOL and Common Logic, in terms of their applicability to the problem of proving program correctness. The issue here isn't just the expressive power of the language, but also the availability and effectiveness of proof tools.
Common Logic itself doesn't seem to offer the ability to formalize proofs within the language.
OWL2 uses its own inference engines.
This is a fascinating topic, as we're interested not only in the formal notation of knowledge but perhaps even more so in the algorithmic processing of knowledge. This set of tools can be called a formal language ecosystem.
Of course, the choice of a formal language, along with its tools, is up to the team solving the problem.
So, there's a dramatic difference between a formal language and the ecosystem of tools for working with texts written in it. I suggested Deepseek (Expert+DeepThink) shed some light on the situation [1].
The topic of formal knowledge processing is crucial. I'm glad you're raising it, at least indirectly.
Alex
[1] https://chat.deepseek.com/share/xuzc9ktfzs2a67plip
Here's the English version:
---
**Question:**
In the work described at
https://www.amazon.science/blog/ec2s-formally-verified-isolation-engine-provides-mathematical-assurance-of-virtual-machine-isolation, the Isabelle/HOL ecosystem is used to prove properties of a specific industrial program. Could this or a similar task be solved in the Common Logic ecosystem, and what tools would need to be used for that?
---
**Answer:**
In short: theoretically yes — isolation properties are formulated in the language of logic, and Common Logic permits this. But practically no — because Common Logic is not a software verification ecosystem but a knowledge representation standard, and solving a task at the AWS Nitro level would require building practically the entire toolchain from scratch that was already ready in Isabelle/HOL.
Let me elaborate.
### What Amazon did with Isabelle/HOL
The AWS team formally verified the "isolation engine" of the Nitro hypervisor. They:
- Created a precise hardware model in Isabelle (MMU, caches, interrupts, etc.);
- Used the AutoCorres tool to translate the hypervisor's C code into a deep embedding in the Isabelle/HOL logic (monadic representation) with automated proof of translation correctness;
- Wrote a specification of "isolation" (no leaks between VMs) as a property in higher-order logic;
- Interactively proved that the generated code model satisfies the specification when running on the hardware model;
- Obtained an end-to-end guarantee that the executable code (after compilation by a verified compiler) preserves the property.
So the work relied on a huge existing foundation: higher-order logic, an automated prover, Sledgehammer, a C-to-deep-embedding translator with correctness proofs, and infrastructure for refinement and code generation.
### What Common Logic (CL) is
Common Logic (ISO/IEC 24707) is a **standard for the semantics and exchange of logical theories**. It defines:
- Syntax (CLIF, CGIF, XCL) for writing formulas in full first-order predicate logic with equality;
- Semantics — classical model theory, interpretations, entailment;
- The ability to name and import ontologies.
CL does **not** contain:
- A built-in theorem prover,
- Tactics or interactive proof tools,
- A refinement mechanism,
- A way to translate C, assembly, or a hardware model into a logical theory,
- Tools for connecting proofs to real executable code (code extraction).
Therefore, CL cannot serve as a direct replacement for Isabelle/HOL — they belong to different tool categories.
### Could this task in principle be solved with CL?
The task of verifying an isolation property is a proof of a theorem within a certain axiomatic theory (describing the behavior of the program and hardware). If this theory were formalized in Common Logic, the required statement would become a theorem of full first-order logic.
Since CL covers all of classical FOL (including infinite models), the expressive power is sufficient. So **theoretically**, the task is reducible to a proof in a CL theory. In practice, however, one would need to assemble the entire stack from scratch.
### What tools would need to be created or employed
Here is the minimal hypothetical set of tools that would be required for "verification in the Common Logic ecosystem":
1. **A C (and/or assembly) to CLIF-theory translator**
An analog of AutoCorres. One would need to define the semantics of a language subset in CL, assign logical axioms about the state to each instruction, and build a formal model of memory/registers. This is enormous work, comparable to building AutoCorres or CompCert. Proofs of translation correctness would also be needed (or, at minimum, one would have to trust the translator).
2. **A formal hardware model in CL**
For the hypervisor, a precise model of the MMU, interrupts, and caches is required — written in CLIF as another theory. Essentially, it would be a conjunction of axioms describing the system's state transitions. This is engineeringly possible, but extremely labor-intensive without higher-order and type support (CL is first-order, no typing, modeling would have to be done through predicates).
3. **A prover (ATP or interactive prover) for CL**
A tool is needed that can accept a theory in CLIF and attempt to prove the target statement. One could use:
- Modern ATPs (Vampire, E, Z3) via translation from CLIF to TPTP FOF (this is relatively straightforward because CLIF and TPTP are close). But they won't "swallow" the proof of the whole system without guiding lemmas.
- An interactive environment is needed where a person breaks down the goal, formulates lemmas, and calls an ATP for subgoals. Such a "Proof General" does not exist in the CL ecosystem. One would have to build a custom proof assistant on top of, say, Hets (Heterogeneous Tool Set), which can work with CL, but again without deep automation.
4. **A guarantee mechanism for the final code**
Even if we proved a theorem about the program model, we need to connect it to the machine code that actually executes. At Amazon, this role is played by a verified compiler (or a formal proof of Isabelle code generation correctness). In a CL-based scheme, an analogous tool would be needed: either a verified compiler that outputs code and simultaneously generates CL axioms about its behavior, or a separate proof of compilation correctness (in the style of CompCert) in the CL language. This is a separate mega-task.
5. **Libraries and tactics for automation**
Isabelle/HOL succeeded largely thanks to Sledgehammer, automatic solvers, and a large number of ready-made tactics and libraries. All of this would have to be written from scratch for CL, or one would use external ATPs without a tactical framework — verifying a program of 5,000+ lines of C in such a mode would be practically impossible within a reasonable timeframe.
### Summary
- **Is it possible?** Yes, in the sense that Common Logic allows writing the entire domain as an axiomatic theory, and the required property as a theorem. The logic is suitable for this.
- **What tools would be needed?** One would have to create: a custom C → CL translator, a hardware model in CL, integration with a powerful ATP, an interactive proof shell, and infrastructure for proving property preservation down to the machine code level. All of this is a gigantic amount of work, vastly exceeding what was already done in Isabelle/HOL.
- **Is it reasonable?** No. Common Logic is a standard for ontology exchange, not an environment for industrial software verification. An attempt to "replicate Amazon" using CL would amount to developing a new proof assistant and verification toolchain in which CL would serve only as a specification language but would offer no advantages over using existing systems such as Isabelle, Coq, or HOL4.
If you're interested in the hypothetical path, I can elaborate in more detail on what the architecture of such a hypothetical CL-based system would look like.
--
All contributions to this forum are covered by an open-source license.
For information about the wiki, the license, and how to subscribe or
unsubscribe to the forum, see http://ontologforum.org/info
---
You received this message because you are subscribed to the Google Groups "ontolog-forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-foru...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/ontolog-forum/2be89986629943ebac1ee59dc561da5c%407f752d9b52a7468ea0f8f1e1df9f914e.