Using Alloy to verify SELinux policies: Seeking advice on neurosymbolic approaches

Questions
1

Hi Alloy community,

We’re working on a paper about automating SELinux policy analysis, and we’re considering using Alloy for formal verification. I recently spoke with Professor @DanielJackson , who suggested that this forum would be a great place to seek input on using Alloy in this context.

Project Overview

Our project aims to address the growing complexity of SELinux policies and the crucial need for ensuring their correctness. As security policies become more complex, it’s increasingly important for distribution/OS maintainers to know exactly what they’re providing to customers. SELinux’s protections are only as strong as the policies provided.

We’re exploring a combination of approaches:

  1. Graph-based policy analysis

    • Parsing SELinux policies into graph databases using Cypher queries
    • Investigating different graph-based anomaly detection techniques

  2. Formal verification methods

    • Exploring the use of SMT for policy verification
    • Converting SELinux policies to SMT formulas to automatically check for inconsistencies and policy violations

  3. Neurosymbolic approach to policy generation

    • Combining formal policy generation with language model guidance
    • Inspired by techniques used in projects like Google DeepMind’s AlphaGeometry

Our proposed system would:

  • Generate initial policy drafts using a policy engine based on basic system information
  • Refine these drafts using a language model trained on SELinux policies
  • Continuously improve policies through analysis tools and language model feedback
  • Incorporate human oversight for critical systems

We believe this approach could significantly streamline SELinux policy creation, making it more efficient and adaptable to evolving security requirements.

Questions for the Alloy Community

We believe Alloy could play a key role in the formal verification aspect of this process. However, we have some questions we’d love to get your insights on:

  1. How readily can SELinux policies and their properties be expressed in Alloy? Has anyone here worked on similar modeling problems?

  2. What’s the best approach to verifying policy correctness using Alloy? We’re considering defining properties to check automatically, but we’re unsure about the specific properties that would be most effective or how to formulate them in Alloy.

  3. Are there any particular challenges or limitations we should be aware of when using Alloy for this kind of policy verification?

  4. Does anyone have experience integrating Alloy with other tools or approaches (like SMT solvers or graph databases) that might be relevant to our project?

  5. Given our interest in combining language models with formal verification, are there any specific considerations or potential pitfalls we should be aware of when trying to integrate Alloy into such a workflow?

We’d greatly appreciate any thoughts, experiences, or suggestions you can share. Your expertise could really help shape our approach to using Alloy in this domain.

Thanks in advance for your input! : )

1 Like
2

Hello! I have used Alloy to model a real-life system and find a hole in it. I have answers for you, but I’m afraid that I’m going to start by asking another question, and possibly throw a bit of cold water on your ambitions:

Is your primary objective to find holes in SELinux, or is your objective to integrate an LLM with a theorem prover / SMT solver? If you try to do both at the same time, I think you will have a harder time than if you choose just one.

The Google DeepMind team did not try to find unknown holes in a large and complex project. Instead, they solved a geometry test with known answers. They threw a very large number of CPU-hours at the feat of solving the same geometry test that one very smart high schooler could solve in a few hours.

I think you may find that proving the consistency of SELinux is harder than passing a geometry test, and if you have fewer PhDs and less computing hardware than Google Deepmind, I do not recommend trying to solve a more difficult problem than Google DeepMind chose to solve.

3

Hi! That’s a cool application of Alloy. I’m reading more into it. Thanks for your insights. We’re trying to find holes in SELinux policies to clarify (not the LSM itself). The goal is to eventually integrate an LLM with a formal verification system. Hope that helps clarify our goals!