Pith. sign in

REVIEW 4 major objections 6 minor 2 cited by

LLMs can't reliably write access policies, but a neurosymbolic tool can summarize them faithfully.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

T0 review · deepseek-v4-flash

2026-08-04 08:23 UTC pith:WUNPDSZO

load-bearing objection A genuinely new neurosymbolic idea with an abstract that overstates both the evaluation and the fidelity guarantee. the 4 major comments →

arxiv 2510.20692 v3 pith:WUNPDSZO submitted 2025-10-23 cs.SE cs.AIcs.FL

Neurosymbolic Characterization for Reliable Access Control Policy Analysis

classification cs.SE cs.AIcs.FL
keywords access control policiesLLM policy synthesisfinite automatamodel countingregular expression summarizationpolicy verificationcloud securitysemantic equivalence
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper argues that large language models are the wrong tool for the core act of access-control policy synthesis: they produce fluent, confident explanations of policy behavior while silently getting the semantics wrong, even when reconstructing a policy from their own explanation. That failure is framed as the Verifiable Synthesis Paradox — precise formal specifications don't need an LLM, and natural-language requirements have no ground truth to verify against. To get the benefits of LLM readability without the unreliability, the authors build PolicySummarizer, which encodes a policy's allowed requests as a finite automaton, extracts an exact regular expression, and asks an LLM to simplify it into something a human can read. A model-counting Jaccard similarity score checks the simplified expression against the exact one, and rejects any simplification that falls below a user-chosen fidelity threshold. The paper reports that on 41 AWS forum policies the simplified summaries retain a mean similarity of 0.889 to the exact expressions, a 2.7x improvement over an SMT-enumeration baseline.

Core claim

PolicySummarizer's claim is that LLM readability can be joined to automata precision provided every simplification is measured. The pipeline encodes the policy as an SMT formula, builds a multi-track deterministic finite automaton whose accepting strings are exactly the allowed requests, and extracts a regular expression via state elimination. It samples accepting strings, asks an LLM to generalize them into a simpler expression, and computes a bounded model-counting Jaccard similarity between exact and simplified languages. If the score meets a user threshold, the simplification is returned; otherwise the exact expression is, so the tool never silently presents an imprecise summary. The sam

What carries the argument

The load-bearing object is the multi-track deterministic finite automaton constructed from the policy's SMT encoding; its accepting strings correspond one-to-one to allowed requests. Around it, three operations carry the argument: state-elimination regex extraction to obtain the exact language; random sampling of accepting strings as the prompt material for the LLM; and the model-counted Jaccard identity J = |A ∧ B| / |A ∨ B|, evaluated on automata with string length bounded at 100, which decides whether the LLM's simplification is close enough to trust.

Load-bearing premise

The whole fidelity guarantee rests on the assumption that every difference that matters between the exact and simplified languages shows up within strings of length 100; differences that only appear in longer strings are invisible to the similarity score.

What would settle it

Construct two regular expressions that accept exactly the same strings of length at most 100 but differ on some longer string (for example, one excludes a single string of length 150); PolicySummarizer's bounded Jaccard similarity will return 1.0 and accept the simplification even though the two languages are not semantically equivalent.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

If this is right

  • An administrator can review simplified regular expressions that describe exactly which resources a policy allows, making human-in-the-loop verification practical where binary allow/deny tools cannot help.
  • The approach summarizes semantic differences: given two policies, it produces expressions for the requests allowed by one but not the other, so policy-change review can target the actual delta.
  • Because the same automaton encodes principal, action, and resource tracks, the summarizer extends to actions and principals by projecting onto a different tuple component.
  • The fidelity check is tunable: a user can set the similarity threshold, and below it the tool falls back to the exact expression, so the summarization is never trusted without measurement.
  • The experimental evidence indicates the simplification quality peaks at a sample size around 1,000 strings, with more examples causing the LLM to overfit.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The abstract reports a mean similarity of 0.93 over 546 AWS, 100 Azure, and 100 GCP policies and a user study raising accuracy from 39% to 93%; the body's experiments cover 41 AWS policies with mean similarity 0.889 and no user study, so readers should treat the abstract's headline numbers as unsubstantiated by this text.
  • The fidelity 'guarantee' is only as strong as the length bound b=100: a simplified expression that differs from the policy only on strings longer than 100 will score 1.0 and be accepted. A natural strengthening is to report the bound alongside the score, or to use unbounded or parameterized counting where possible.
  • The same automaton-and-model-counting chassis could be applied to other configuration artifacts that admit a regular language — network firewalls, routing filters, or URI whitelists — wherever an LLM's paraphrase needs a formal backstop.
  • One testable extension: instead of a single threshold on Jaccard similarity, return the LLM simplification together with examples of the symmetric difference, so a reviewer sees not just a score but the actual requests the simplification adds or drops.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

4 major / 6 minor

Summary. The paper studies LLM capabilities for access-control policy synthesis and comprehension, and proposes PolicySummarizer, a tool that combines automata-based policy encoding with LLM-based regex simplification. The pipeline (Algorithm 1) encodes a policy into an SMT formula, builds a multi-track DFA, extracts a regular expression R_DFA, samples accepted strings, prompts an LLM to produce a simplified regex R_LLM, and computes a bounded-length Jaccard similarity (Eq. 5, Algorithm 3) between the two. If the similarity meets a user threshold, R_LLM is returned; otherwise R_DFA is returned. The evaluation in §6 covers 41 AWS Quacky policies, reporting mean similarity 0.889 and a 2.7x improvement over an emulated Z3-based baseline. The abstract additionally claims results on 546 AWS, 100 Azure, and 100 GCP policies, a mean similarity of 0.93, and a user study raising accuracy from 39% to 93%, none of which appear in the body.

Significance. If the results were fully supported, the work would fill a real gap: producing human-readable, quantitatively vetted summaries of allowed requests, with a fallback to a precise regex when the LLM simplification is poor. The automata-to-regex extraction and the use of model counting to filter LLM outputs are sensible and potentially reusable. The paper's main strengths are the concrete algorithms (Algorithms 1–3) and the idea of a neurosymbolic pipeline with a formal fallback. However, the current evidence is much narrower than the abstract claims, and the 'fidelity guarantee' is only a bound-dependent approximation. The contribution is promising but needs substantial revision to be reliable.

major comments (4)
  1. [Abstract; §6.1, §6.2] The abstract states that PolicySummarizer was evaluated on 546 AWS, 100 Azure, and 100 GCP policies, achieves a mean similarity of 0.93, and that a user study raised accuracy from 39% to 93%. The experimental section contains none of this: §6.1 describes only the 41 original AWS Quacky policies, §6.2 reports a mean similarity of 0.889, no Azure or GCP policies are evaluated, and no user study appears anywhere in the manuscript. The 2.7x improvement is specifically against an emulated Z3 baseline (RQ3), not a general SMT baseline. These are the headline claims, so the mismatch is load-bearing and must be resolved by either adding the missing experiments or rewriting the abstract to match the body.
  2. [§5.3, Eq. (5); §6.1; §7.1] The fidelity guarantee claimed in the abstract is not delivered by Algorithm 3. Eq. (5) computes Jaccard similarity over accepting strings of length at most b, and §6.1 fixes b=100. Two regexes can agree on every string up to length 100 and differ on longer strings; Eq. (5) would then return 1.0 and the simplified regex would be accepted even though it does not characterize the policy's language. The paper's own §7.1 acknowledges that usefulness depends on the bound, and justifies b=100 by manual inspection of AWS policies. That is a domain heuristic, not a proof. Since exact language equivalence and inclusion are decidable for DFAs, the 'guarantee' could be made rigorous; as written, it is a bounded approximation and the terminology should be adjusted accordingly.
  3. [§5.3, §6.1] The evaluation exhibits selection circularity. In Algorithm 1, the LLM is given strings sampled from R_DFA and asked to produce a simplified regex; the similarity is then measured against the same R_DFA. §6.1 states that the LLM is queried three times and the best of three results is taken. This best-of-three selection on the evaluation policies can inflate the reported Jaccard scores. The paper should report the distribution over independent runs, or use a held-out set, to show the improvement is not an artifact of selection.
  4. [Abstract; §5.2] The paper's central contribution is described in the abstract as generating 'precise human-readable characterizations of requests allowed by a policy.' However, §5.2 shows that the implemented tool projects away all tuple elements except the resource before regex extraction, so it characterizes allowed resources only. The abstract's phrasing is therefore broader than the actual implementation. The authors should either extend the technique to full requests or state the resource-only scope in the abstract.
minor comments (6)
  1. [Title] The arXiv title is 'Neurosymbolic Characterization for Reliable Access Control Policy Analysis', but the manuscript's title is 'Exploring Large Language Models for Access Control Policy Synthesis and Summarization'. The title should be aligned with the submitted version.
  2. [Eq. (1)] Equation (1) appears to be missing a negation: as typeset, it says 'there exists an allow rule and there exists a deny rule' rather than 'and no deny rule exists', contradicting the prose. Please fix the rendering.
  3. [§6.2] The text refers to 'Claude-4.0-sonne' twice; this should be 'Claude-4-Sonnet'.
  4. [Abstract / Availability] The abstract promises 'We release PolicySummarizer as an open-source tool,' but the body contains no repository URL or availability section. Please add the link or remove the claim.
  5. [Figures 6 and 7] The captions for Figures 6 and 7 do not describe the axes or units; for example, it is unclear whether the y-axis in Figure 6 is Jaccard similarity or regex length. Descriptive captions would improve reproducibility.
  6. [Algorithm 2] The constants r=1.01 and thresh=0.10 in Algorithm 2 are not justified. A brief explanation of how these values were chosen would help readers reproduce the sampling procedure.

Circularity Check

0 steps flagged

No load-bearing circularity; the central fidelity check is an independent formal computation. Minor self-citation and evaluation-selection effects do not reduce the result to its own inputs.

full rationale

Walking the claimed derivation chain: Algorithm 1 builds an MDFA A_P from JPK, extracts R_DFA via state elimination, samples strings from R_DFA, prompts an LLM for a simplified R_LLM, and Algorithm 3 / Eq. (5) computes J by model-counting the intersection and union DFAs of R_DFA and R_LLM under a length bound b. This comparison is an independent formal computation over the DFA languages, not over the sample used to prompt the LLM; a poor LLM output can produce a low J, so the reported similarity is not forced by construction. The 'fidelity guarantee' is weakened by the length bound (b=100), and Section 7.1 admits 'model counting on strings can be infinite and thus the usefulness of results depends on the bound' — this is a correctness/validity threat, not a circular reduction. Likewise, querying the LLM three times and taking the best result, and tuning the sample size on the same policies, are evaluation-selection effects rather than fitted parameters renamed as predictions. Self-citations to the authors' prior tools (ABC, Quacky) are to public, tool-backed artifacts and are not invoked as a uniqueness theorem. The abstract/body mismatches (546/100/100 policies vs. 41 AWS policies; 0.93 vs. 0.889; user study absent in the body) are reporting inconsistencies, not circularity. No step reduces to its own input; score 2 reflects only minor self-citation and selection concerns.

Axiom & Free-Parameter Ledger

5 free parameters · 3 axioms · 0 invented entities

No new physical or conceptual entities are postulated; the paper's central load is carried by tuning parameters (b, n, t, model, best-of-k) and by the assumption that bounded model counting stands in for semantic equivalence.

free parameters (5)
  • string length bound b = 100
    All model-counting similarity scores in Eq. 5 are computed over strings of length ≤100; chosen by manual inspection of AWS policies (Section 6.1), so long-string deviations are invisible.
  • sample size n = 1000 (reported best in RQ2)
    Sample count for LLM regex generation; RQ2 shows similarity rises to 1000 then decreases, and 1000 is used for the headline comparison to baseline, suggesting selection on the same benchmark.
  • similarity threshold t = not reported
    User-configured acceptance threshold in Algorithm 1; no value is given, so the 'guarantee' level of the returned summaries is unspecified.
  • LLM choice and best-of-k = Claude-4-Sonnet, k=3
    Model chosen because it 'worked best' on the same evaluation policies, and the best of 3 generations is kept, inflating average similarity relative to a single draw.
  • sampling parameters r, thresh = r=1.01, thresh=0.10
    Hard-coded in Algorithm 2 to make Kleene-star sampling terminate; biases samples toward short strings, affecting what the LLM sees.
axioms (3)
  • domain assumption The MDFA constructed from JPK exactly characterizes all satisfying solutions to the SMT encoding (L(AP) = Allow(P)).
    Relies on the ABC model-counting tool [4] and the Quacky policy model [14,15]; assumed sound for the AWS policy subset considered.
  • ad hoc to paper Bounding string length at 100 is sufficient to capture behavior relevant for the policies studied.
    Section 6.1 sets b=100 after manual analysis; this is a domain assumption that makes the fidelity guarantee bounded rather than absolute.
  • ad hoc to paper Randomly sampled accepted strings (Algorithm 2) are representative enough for the LLM to infer a regex that generalizes the policy.
    No coverage or diversity guarantee is provided; rare paths may be missed and the similarity check over bounded strings would not catch it.

pith-pipeline@v1.3.0-alltime-deepseek · 16760 in / 15675 out tokens · 137349 ms · 2026-08-04T08:23:31.756675+00:00 · methodology

0 comments
read the original abstract

Access control policies are reliability-critical configuration artifacts in cloud systems, yet administrators frequently struggle to verify that a policy permits exactly what they intend. This verification gap cannot be remedied by using LLMs to synthesize policies: we find that reasoning and non-reasoning LLMs fluently explain policy behavior but cannot reason about policy semantics with reliability-grade precision, even when the specification is the LLM's own explanation. We formulate this impasse as the Verifiable Synthesis Paradox: the verification gap persists regardless of how the policy was authored. To remedy this, we introduce PolicySummarizer, a neurosymbolic tool that pairs finite-state automata with an LLM-based simplification to generate precise human-readable characterizations of requests allowed by a policy. PolicySummarizer uses model counting to guarantee the fidelity of the generated characterization by rejecting characterizations that fall below a user-configured threshold in favor of the formally derived one. On 546 AWS, 100 Microsoft Azure, and 100 Google Cloud Platform policies, PolicySummarizer achieves a mean similarity score of 0.93 and a 2.7x improvement over an SMT-based baseline. In a user study, PolicySummarizer raised policy-change-review accuracy from 39% to 93% on the hardest sub-task while reducing self-reported mental demand. We release PolicySummarizer as an open-source tool.

Figures

Figures reproduced from arXiv: 2510.20692 by Adarsh Vatsa, Bethel Hall, William Eiers.

Figure 1
Figure 1. Figure 1: LLM Policy Comprehension and Reconstruction results. [PITH_FULL_IMAGE:figures/full_fig_p006_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Comprehensive Policy Comprehension Assessment. [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Initial policy allowing nothing (left), modified policy that allows access to specific resources (right). [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Projected DFA representing allowed resources from the motivating example in Figure [PITH_FULL_IMAGE:figures/full_fig_p013_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Regular expression extraction and generation process for the DFA constructed in Figure [PITH_FULL_IMAGE:figures/full_fig_p013_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Results of the resource characterizations for original policies in the Quacky dataset. [PITH_FULL_IMAGE:figures/full_fig_p014_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Comparison of average similarity measure based on number of strings used during generalization [PITH_FULL_IMAGE:figures/full_fig_p016_7.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. AutoCedar: An Agentic Framework for Verifier-Guided Access Control Policy Synthesis

    cs.SE 2026-07 conditional novelty 6.5

    AutoCedar first builds a reviewed, checkable authorization boundary from natural-language requirements, then synthesizes Cedar policies against that fixed target with verifier-guided repair, solving all 221 CedarBench tasks.

  2. Combinatorial Allocation Bandits with Nonlinear Arm Utility

    cs.LG 2026-03 unverdicted novelty 6.0

    CAB maximizes arm satisfaction in contextual combinatorial matching under GLM feedback, with UCB/TS algorithms whose regret matches combinatorial contextual lower bounds up to logs.

Reference graph

Works this paper leans on

41 extracted references · 2 canonical work pages · cited by 2 Pith papers

  1. [1]

    Abad-Peiro, Hervé Debar, Thomas Schweinberger, and Peter Trommler

    Jose L. Abad-Peiro, Hervé Debar, Thomas Schweinberger, and Peter Trommler. 1999.PLAS — Policy Language for Authorizations. Technical Report RZ 3126. IBM Research Division. http://citeseer.nj.nec.com/abad-peiro99plas.html

  2. [3]

    aleak [n. d.]. Another misconfigured Amazon S3 server leaks data of 50,000 Australians. https://www.scmagazineuk. com/another-misconfigured-amazon\-s3-server-leaks-data-of-50000-australians/article/705125/

  3. [4]

    Abdulbaki Aydin, William Eiers, Lucas Bang, Tegan Brennan, Miroslav Gavrilov, Tevfik Bultan, and Fang Yu. 2018. Parameterized model counting for string and numeric constraints. InProceedings of the 2018 ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/SIGSOFT FSE 2018, Lake Buena ...

  4. [5]

    azureflaw [n. d.]. Microsoft Azure cloud vulnerability is the ‘worst you can imagine’. https: //www.theverge.com/2021/8/27/22644161/microsoft-azure-database-vulnerabilty-chaosdb?fbclid= IwAR2nKV8uslH4EGDslnogYT4ulQRGz7NsD0xuIb3lgK2sP1-WG_O1tJbR-eE

  5. [6]

    John Backes, Pauline Bolignano, Byron Cook, Catherine Dodge, Andrew Gacek, Kasper Luckow, Neha Rungta, Oksana Tkachu, and Carsten Varming. 2018. Semantic-based Automated Reasoning for AWS Access Policies using SMT. In Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design (FMCAD 2018), Austin, Texas, USA, October 30 - November 2, 2018. 1–9

  6. [7]

    Alberto Bartoli, Andrea De Lorenzo, Eric Medvet, and Fabiano Tarlao. 2016. Inference of Regular Expressions for Text Extraction from Examples.IEEE Transactions on Knowledge and Data Engineering28, 5 (2016), 1217–1230. Exploring Large Language Models for Access Control Policy Synthesis and Summarization 19 doi:10.1109/TKDE.2016.2515587

  7. [8]

    Geert Jan Bex, Frank Neven, Thomas Schwentick, and Stijn Vansummeren. 2010. Inference of concise regular expressions and DTDs.ACM Trans. Database Syst.35, 2, Article 11 (may 2010), 47 pages. doi:10.1145/1735886.1735890

  8. [9]

    Malik Bouchet, Byron Cook, Bryant Cutler, Anna Druzkina, Andrew Gacek, Liana Hadarean, Ranjit Jhala, Brad Marshall, Dan Peebles, Neha Rungta, Cole Schlesinger, Chriss Stephens, Carsten Varming, and Andy Warfield. 2020. Block Public Access: Trust Safety Verification of Access Control Policies. InProceedings of the 28th ACM Joint Meeting on European Softwar...

  9. [10]

    Dougherty, Kathi Fisler, and Shriram Krishnamurthi

    Daniel J. Dougherty, Kathi Fisler, and Shriram Krishnamurthi. 2006. Specifying and Reasoning About Dynamic Access-Control Policies. InAutomated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, W A, USA, August 17-20, 2006, Proceedings (Lecture Notes in Computer Science, Vol. 4130), Ulrich Furbach and Natarajan Shankar (Eds.). Springer...

  10. [11]

    dowjonesleak [n. d.]. Cloud Leak: WSJ Parent Company Dow Jones Exposed Customer Data. https://www.upguard. com/breaches/cloud-leak-dow-jones

  11. [12]

    Serge Egelman, Andrew Oates, and Shriram Krishnamurthi. 2011. Oops, I Did It Again: Mitigating Repeated Access Control Errors on Facebook. InProceedings of the SIGCHI Conference on Human Factors in Computing Systems(Vancouver, BC, Canada)(CHI ’11). ACM, New York, NY, USA, 2295–2304. doi:10.1145/1978942.1979280

  12. [13]

    William Eiers, Ganesh Sankaran, and Tevfik Bultan. 2023. Quantitative Policy Repair for Access Control on the Cloud. InProceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis(Seattle, WA, USA) (ISSTA 2023). Association for Computing Machinery, New York, NY, USA, 564–575. doi:10.1145/3597926.3598078

  13. [14]

    William Eiers, Ganesh Sankaran, Albert Li, Emily O’Mahony, Benjamin Prince, and Tevfik Bultan. 2022. Quantifying permissiveness of access control policies. InProceedings of the 44th International Conference on Software Engineering (Pittsburgh, Pennsylvania)(ICSE ’22). Association for Computing Machinery, New York, NY, USA, 1805–1817. doi:10. 1145/3510003.3510233

  14. [15]

    William Eiers, Ganesh Sankaran, Albert Li, Emily O’Mahony, Benjamin Prince, and Tevfik Bultan. 2023. Quacky: Quantitative Access Control Permissiveness Analyzer. InProceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering(<conf-loc>, <city>Rochester</city>, <state>MI</state>, <country>USA</country>, </conf-loc>)(ASE ’22)....

  15. [16]

    Kathi Fisler and Shriram Krishnamurthi. 2010. A model of triangulating environments for policy authoring. InSACMAT 2010, 15th ACM Symposium on Access Control Models and Technologies, Pittsburgh, Pennsylvania, USA, June 9-11, 2010, Proceedings, James B. D. Joshi and Barbara Carminati (Eds.). ACM, 3–12. doi:10.1145/1809842.1809847

  16. [17]

    Fisler, S

    K. Fisler, S. Krishnamurthi, L. A. Meyerovich, and M. C. Tschantz. 2005. Verification and Change-Impact Analysis of Access-Control Policies. InProceedings of the 27th International Conference on Software Engineering (ICSE 05). 196–205

  17. [18]

    Fisler, S

    K. Fisler, S. Krishnamurthi, L. A. Meyerovich, and M. C. Tschantz. 2005. Verification and Change-Impact Analysis of Access-Control Policies. InProceedings of the 27th International Conference on Software Engineering. St. Louis, Missouri, 196–205

  18. [19]

    J. E. Hopcroft and J. D. Ullman. 1979.Introduction to automata theory, languages, and computation. Addison-Wesley, Reading, Massachusetts

  19. [20]

    Xinyi Hou, Yanjie Zhao, Yue Liu, Zhou Yang, Kailong Wang, Li Li, Xiapu Luo, David Lo, John Grundy, and Haoyu Wang

  20. [21]

    Graham Hughes and Tevfik Bultan. 2008. Automated verification of access control policies using a SAT solver.STTT 10, 6 (2008), 503–520. doi:10.1007/s10009-008-0087-9

  21. [22]

    Sushil Jajodia, Pierangela Samarati, Maria Luisa Sapino, and V. S. Subrahmanian. 2001. Flexible support for multiple access control policies.ACM Transactions on Database Systems26, 2 (2001), 214–260. http://doi.acm.org/10.1145/ 383891.383894

  22. [23]

    Jajodia, P

    S. Jajodia, P. Samarati, and V. S. Subrahmanian. 1997. A logical language for expressing authorizations. InProceedings of the 1997 IEEE Symposium on Security and Privacy. IEEE Press, Oakland, CA, USA, 31–42. http://citeseer.nj.nec.com/ jajodia97logical.html

  23. [24]

    Sushil Jajodia, Pierangela Samarati, V. S. Subrahmanian, and Eliza Bertino. 1997. A unified framework for enforcing multiple access control policies. InSIGMOD’97. Tucson, AZ, 474–485. http://citeseer.nj.nec.com/jajodia97unified.html

  24. [25]

    Sakuna Harinda Jayasundara, Nalin Asanka Gamagedara Arachchilage, and Giovanni Russello. 2024. SoK: Access Control Policy Generation from High-level Natural Language Requirements.ACM Comput. Surv.57, 4, Article 102 (Dec. 2024), 37 pages. doi:10.1145/3706057

  25. [26]

    Sherifdeen Lawal, Xingmeng Zhao, Anthony Rios, Ram Krishnan, and David Ferraiolo. 2024. Translating Natu- ral Language Specifications into Access Control Policies by Leveraging Large Language Models. In2024 IEEE 6th 20 Adarsh Vatsa, Bethel Hall, and William Eiers International Conference on Trust, Privacy and Security in Intelligent Systems, and Applicati...

  26. [27]

    Mina Lee, Sunbeom So, and Hakjoo Oh. 2016. Synthesizing regular expressions from examples for introductory automata assignments. InProceedings of the 2016 ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences(Amsterdam, Netherlands)(GPCE 2016). Association for Computing Machinery, New York, NY, USA, 70–80. doi:10.1145/29...

  27. [28]

    Yeting Li, Zhiwu Xu, Jialun Cao, Haiming Chen, Tingjian Ge, Shing-Chi Cheung, and Haoren Zhao. 2021. FlashRegex: deducing anti-ReDoS regexes from examples. InProceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering(Virtual Event, Australia)(ASE ’20). Association for Computing Machinery, New York, NY, USA, 659–671. doi:10...

  28. [29]

    Daye Nam, Andrew Macvean, Vincent Hellendoorn, Bogdan Vasilescu, and Brad Myers. 2024. Using an LLM to Help With Code Understanding. arXiv:2307.08177 [cs.SE] https://arxiv.org/abs/2307.08177

  29. [30]

    Dougherty, Kathi Fisler, and Shriram Krishnamurthi

    Timothy Nelson, Christopher Barratt, Daniel J. Dougherty, Kathi Fisler, and Shriram Krishnamurthi. 2010. The Margrave Tool for Firewall Analysis. InProceedings of the 24th International Conference on Large Installation System Administration(San Jose, CA)(LISA’10). USENIX Association, USA, 1–8

  30. [31]

    Maria Paratore, Eda Marchetti, and Antonello Calabrò. 2025. From Plain English to XACML Policies: An AI-Based Pipeline Approach. 85–96. doi:10.5220/0013357200003896

  31. [32]

    Rubio-Medrano, Akash Kotak, Wenlu Wang, and Karsten Sohr

    Carlos E. Rubio-Medrano, Akash Kotak, Wenlu Wang, and Karsten Sohr. 2024. Pairing Human and Artificial Intelligence: Enforcing Access Control Policies with LLMs and Formal Specifications. InProceedings of the 29th ACM Symposium on Access Control Models and Technologies(San Antonio, TX, USA)(SACMAT 2024). Association for Computing Machinery, New York, NY, ...

  32. [33]

    2001.Foundations of Security Analysis and Design

    Pierangela Samarati and Sabrina De Capitani di Vimercati. 2001.Foundations of Security Analysis and Design. Springer Verlag, Chapter 3, 137–196

  33. [34]

    Ravi Sandhu and Pierangela Samarati. 1996. Authentication, access control, and audit.Comput. Surveys28, 1 (1996), 241–243. http://doi.acm.org/10.1145/234313.234412

  34. [35]

    Sandhu and Pierangela Samarati

    Ravi S. Sandhu and Pierangela Samarati. 1994. Access Control: Principles and Practice.IEEE Communications Magazine 32, 9 (1994 1994), 40–48. http://citeseer.nj.nec.com/article/sandhu94access.html

  35. [36]

    Andreas Schaad and Jonathan Moffet. 2002. A Lightweight Approach to Specification and Analysis of Role-based Access Control Extensions. In7th ACM Symposium on Access Control Models and Technologies (SACMAT 2002)

  36. [37]

    Pranav Subramaniam and Sanjay Krishnan. 2025. DePLOI: Applying NL2SQL to Synthesize and Audit Database Access Control. arXiv:2402.07332 [cs.DB] https://arxiv.org/abs/2402.07332

  37. [38]

    Adarsh Vatsa, Pratyush Patel, and William Eiers. 2025. Synthesizing Access Control Policies using Large Language Models. arXiv:2503.11573 [cs.SE] https://arxiv.org/abs/2503.11573

  38. [39]

    verizonleak [n. d.]. 14 MEEELLION Verizon subscribers’ details leak from crappily configured AWS S3 data store. https://www.theregister.co.uk/2017/07/12/14m_verizon_customers_details_out/

  39. [40]

    John Zao, Hoetech Wee, Jonathan Chu, and Daniel Jackson. 2003. RBAC Schema Verification Using Lightweight Formal Model and Constraint Analysis. InProceedings of the eighth ACM symposium on Access Control Models and Technologies

  40. [41]

    Shuai Zhang, Xiaodong Gu, Yuting Chen, and Beijun Shen. 2023. InfeRE: Step-by-Step Regex Generation via Chain of Inference. arXiv:2308.04041 [cs.AI] https://arxiv.org/abs/2308.04041

  41. [2024]

    arXiv:2308.10620 [cs.SE] https://arxiv.org/abs/2308.10620

    Large Language Models for Software Engineering: A Systematic Literature Review. arXiv:2308.10620 [cs.SE] https://arxiv.org/abs/2308.10620