Using AI to Autoformalize Network Security Properties into 5STARS

Formal verification has two core facets:

1. Specifying correct behavior in a formal language.
2. Verifying that an implementation satisfies that specification.

This summer I interned at Galois and worked with a project called 5STARS, which is a tool for formally verifying the security of networks. This tool excels at the second facet, but existing workflows struggled with the first. Using 5STARS, you can automatically check a wide variety of important properties of a network. However, the translation of high-level security properties into formalized properties (i.e. a specification) that 5STARS can automatically verify is still a bottleneck.

My project this summer was to experiment with using AI to help translate high-level security properties into formalized properties in 5STARS. This task is commonly referred to as autoformalization. In particular, my goal was to develop an integration (via MCP) into common AI agent clients (such as Codex, Antigravity, Open Code, etc.) that assists users with 5STARS to justify the security posture of their network.

Developing an MCP Server

My goal was to develop a tool that would be easy for experts and non-experts alike to use in a relatively free-form manner with whatever AI interface they like. To accomplish this, I turned to the Model Context Protocol (MCP), which is an emerging standard introduced in late 2024. This protocol specifies a convenient way for servers to locally or remotely expose their endpoints to any AI client. Common examples include interfaces for AI agents to interact with services like GitHub, Linear, Google Maps, etc. While command-line interfaces are designed for human users, MCP endpoints are designed specifically to integrate into agentic AI workflows (however, there is still significant debate about the utility of having MCP as a separate protocol). For my use case, MCP turned out to be very useful because it allowed me to easily build on top of existing tools and keep fine-grained control over how the AI agent uses the tools I implement.

I designed an MCP server that wraps the 5STARS CLI in order to implement some custom functionality. Below are a few key takeaways from what worked well.

Fine-grained feedback. Tools designed for humans often assume that the human can intelligently infer or search for proper context regarding input and output. While modern AI tools can emulate this surprisingly well, they still often fail to complete a straightforward task consistently in the exact manner intended. One way to address this limitation is to make implicit context more explicit. For example, an error message from a tool can include the referenced passage embedded directly within the diagnostic message itself rather than just referring to the source line number.

Literate programming support. While allowing an AI to write prose and code in whatever format it likes maximizes creativity, it comes at the cost of reliability and analyzability. For example, I'd like to know that the final output from an AI workflow can be grounded in the intermediate steps it performed. One approach I found that enforced this in a feasible way was literate programming. Using literate programming, the AI can support its natural language prose with interleaved code blocks containing assertions that can be automatically checked by 5STARS. While this does not guarantee that the prose is always going to be truthful, it does align the prose exactly with the formalized and automatically interpreted grounding that should support it.

Using an MCP Server as a Harness

While developing the original version of the MCP server, the core issue I consistently encountered was reliability. After implementing the augmentations I mentioned above to address the basic inadequacies common with AI agents, it became extremely difficult to do further evaluation and iteration because the results were highly inconsistent.

Taking a step back, I considered the question of "reliability with respect to what?" Sure, the agent was inferring very different formal specifications of network security each run, and they weren't all correct, but which were more correct than others? Going forward, I needed to more formally consider the meta-specification I was judging the AI-inferred specifications by.

I drew on a few key resources, including:

• NIST SP 800-53 Rev. 5: Security and privacy controls for information systems and organizations.
• MITRE ATT&CK: A knowledge base of adversary tactics and techniques based on real-world observations.

I extracted from these resources a collection of natural language security properties based on guidelines and attack mitigation strategies.

With these security properties as a set of high-level specifications to start with, I could much more effectively ensure the agent would infer relevant formalizations that could now be judged against the given high-level properties. I divided up this work into two phases: (1) specializing the high-level properties to the particular network of interest, (2) formalizing those specialized properties so they can be checked by 5STARS.

To ensure that these phases were carried out in the correct sequence and that all work was done comprehensively, I expanded the role of the MCP server to be more akin to what is often called a harness. My project integrates into existing general harnesses, which already have their own systems for guiding an AI agent through a complex series of tasks, so I needed to design this harness extension to hook into how a core harness already works in a lightweight way through an MCP integration. Here's how I accomplished this:

• The MCP server has an internal state tracking the accumulated progress of the agent as it runs through various workflows.
• The tools exposed by the MCP server integrate with the MCP server state to determine which tools are available and how they can modify the state.
• The workflow phases are implemented as sets of tools. Among these tools is a special "diagnostics" tool that reports diagnostics about the current status of the phase, including what tasks still need to be done in order to complete the phase and guidelines for using available tools.

A very nice feature of this design is that the accumulated work of the agent is preserved in an external artifact managed by programs I wrote that the agent can't modify. Often AI agents take actions in an open-ended workspace, where they can read, write, and reorganize files as they wish. This can make it difficult for programmatic tools to analyze the work that the agent has done without requiring a comprehensive set of project management tools. In contrast, using the MCP server as a lightweight harness allows me to have complete control over how the AI agent accumulates its work in a completely structured way. For example, I can enforce that certain aspects of the MCP server state are monotonic, where the agent cannot accidentally revert progress.

Additional secondary benefits of this design were easy support for a pretty browser-based UI for viewing the agent's progress (including an interactive visualization of the network topology), and snapshotting (where a copy of the MCP server state is a self-contained snapshot of all the agent's work so far, not including the conversation history of course).

LLMs and DSLs

Until recently, even state-of-the-art LLMs had significant difficulty working with custom DSLs. They were too well-trained on the most common programming languages in their training data, and failed even relatively simple extrapolation. Still today, people argue about how important it is to take into account an LLM's proficiency when choosing a programming language for a project. However, this inadequacy has changed significantly since just a few years ago.

I developed custom DSLs for several different use cases in this project to great success! In one case I needed to define a particular refinement of the kinds of properties that the agent is allowed to write and then check with 5STARS. If I just gave the agent access to all 5STARS language features, then it would often run into issues, for example:

• The agent would get confused by the unfamiliar syntax and features that I intentionally omitted from my instructions (because there was only a particular refinement of those properties that I wanted it to be able to write in the first place).
• The agent would get confused by error messages reported by the 5STARS CLI, since the CLI assumes that the entire language is available to work with.
• In order to do static analysis on the properties that the agent wrote, I needed to write ad hoc parsers to extract that info, which could often be in irregular formats depending on how liberally the agent used the syntax.

To provide the agent with a more convenient interface, I defined a specialized DSL just for the particular properties that the AI should be allowed to write. Yes, I did need to implement a parser and extremely simple type checker, which would likely have been prohibitive for the scope of this project if the range of properties to allow was very complicated. However, since the properties I was interested in were quite constrained, this entire implementation was eminently tractable. And along the way I could define very fine-grained feedback in error messages resulting from parsing and type checking.

Another case where I used a custom DSL was in the custom format for prose related to the network the agent is analyzing. One very common issue with LLMs is hallucination, where an LLM confidently asserts incorrect information (often in the form of inventing a reference that doesn't exist). Hallucinations have proven very insidious because they are usually mixed in with other true authoritatively presented claims, and so are difficult to catch for lay (or even expert) readers. In addition to having each analysis attached to a formalized check, I also needed to implement some static analysis on the natural language proofs written to explain the significance of the formalized checks that are run. To accomplish this, I defined a simple hypertext format where the agent can include hypertext-like links in the natural language prose of its explanations, and then those links can reliably be parsed out and checked against the known ontology of the network. For example, if the AI refers to a device or an interface or a subnet in its explanation, this process will check that the object actually does exist in the network. If the object doesn't exist, then this process will report the discovered issues back to the agent, giving it an opportunity to check its work and come up with correctly grounded prose.

LLMs as Beta Testers

As a side note, I found one of the most productive uses of LLMs during development was as a beta tester. Writing a complete test suite upfront to cover all intended uses can be overly cumbersome. While fuzzing is a powerful means of unstructured testing, it is difficult to effectively apply to a system like this where much of the interaction is done through natural language. So why not use an LLM as an informal "fuzzer" (i.e., beta tester)?

My project is designed to be used by both humans and LLMs alike, but it's easy to have an LLM play the role of whatever user you like. I just asked an agent to go through a workflow as described in natural language and then report back to me what issues it encountered. Very often it accurately reported real issues that led me either to rethink my design or to encode the correct behavior as unit tests. Because the AI is infinitely patient and loves nothing more than to fix things, it was a very pleasant experience using the AI beta tester to rapidly find basic UX issues that would have taken much more time and effort to discover manually or that would have been tricky to encode as static properties without initial manual testing.

Conclusions

I went into this internship curious about how far I could get doing autoformalization using AI. I had many reasons to be skeptical due to the stochastic and unreliable nature of LLMs. In particular, LLMs seem to work best when they are interacting with a formalized environment that can provide detailed and corrective feedback. Autoformalization doesn't quite match this ideal situation because of course it is the process of inferring the formal specifications, which means we don't already have formal specifications to judge its results by.

Now at the end of the summer (at the time this piece was written), I am pleasantly surprised with the progress I was able to make developing a relatively advanced augmentation for interactive agentic systems that enables the agent to be proactive and exploratory while ensuring thoroughness and adherence to the high-level structure specified by human users.

My experience suggests that lightweight finite state machine (FSA)-based harnesses integrated via MCP and specialized DSLs are effective techniques for many projects for integrating AI into workflows related to formal verification. I noticed that many others at Galois are working on similar workflows related to autoformalization and/or formal verification more generally, so I'm curious to see the evolution of alternative approaches or extensions of my project.

‍

‍

Distribution Statement A: Approved for Public Release

This material is based upon work supported by the Naval Surface Warfare Center-Corona Division (NSWC-Corona) under Contract No. N6426725C7016. Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the NSWC-Corona.