Bounded Satisfiability Checking for Early Legal Compliance Verification

Early verification of legal compliance is crucial to avoid consequences such as violating regulations like GDPR. Through bounded satisfiability checking using Metric First-order Temporal Logic (MFOTL), this research focuses on system design verification for regulatory compliance. The study addresses finitesatisfiability and k-bounded satisfiability of MFOTL formulas, providing insights into ensuring system properties are met within specified constraints.

• Legal Compliance
• Verification
• Bounded Satisfiability
• Metric First-order Temporal Logic
• System Design

nicksongi Follow

Uploaded on Sep 21, 2024 | 0 Views

Download Presentation

Please find below an Image/Link to download the presentation.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

Presentation Transcript

1. Early Verification of Legal Compliance via Bounded Satisfiability Checking Nick Feng, Lina Marsso, Mehrdad Sabetzadeh, Marsha Chechik CAV 2023

2. Context: Regulatory Compliance Comply Regulations (e.g., GDPR) System Violations lead to consequences GDPR: General Data Protection Regulation 2 https://www.enzuzo.com/blog/biggest-gdpr-fines

3. Motivation: Verification on System Design System Design Formal Specification (Property) Formal Specifications (Requirements) Check: Requirements Property A violation scenario Compliant 3

4. Motivation: Verification on System Design Time and data constraints System Design MFOTL Specification (Property) MFOTL Specifications (Requirements) Check MFOTL finitesatisfiability : (Requirements Property) SAT UNSAT Safety properties A finite violation scenario Compliant 4 MFOTL: Metric First-order Temporal Logic

5. Background: Metric First-order Temporal Logic Metric First-order Temporal Logic (MFOTL) [1] : 1. Support metric temporal operators: (????? 0,1000???) Allow specification of both data and time constraints 2. Support quantifiers : ?? (????? ?,? 0,100 ???? ?,? ) MFOTL has used for formalizing regulations for runtime verification [2] [1] MONPOLY: Monitoring usage-control policies. D. Basin, M. Harvan, F. Klaedtke, E. Z linescu, RV 2012. [2]Monitoring the GDPR. A. Emma, D. Basin, and S. Debois, ESORICS 2019. 5

6. Problem: MFOTL Finite Satisfiability An MFTOL formula is finitely satisfiable if and only if there exists a finite trace that satisfies the MFTOL formula. ?? (???? ?,? 0,100 ????? ?,? ) What values that hold for what relations at which time point? Number of time point? Time value each time point? Undecidable* 6

7. Problem: Bounded MFOTL Satisfiability A MFTOL formula is k-bounded satisfiable If and only if there exists a trace of volume at most k that satisfies the MFTOL formula. ?? (???? ?,? 0,100 ????? ?,? ) The trace of the volume is bounded by k Volume =5 7

8. Problem: Bounded MFOTL Satisfiability Our focus System Design MFOTL Specification (Property) MFOTL Specifications (Requirements) Check MFOTL k-bounded satisfiability of: (Requirements Property) UNSAT K-bounded UNSAT SAT A K-bounded violation scenario K-bounded compliant Compliant 8

9. Contributions 1. MFOTL bounded satisfiability 2. Decision procedure for MFOTL bounded satiability a. Reducing to FOL* bounded satisfiability b. DeterminingFOL* bounded satisfiability via incremental approximation 9

10. Outline I. Problem: Bounded MFOTL satisfiability II. Approach: MFOTL bounded satisfiability checking 1. Reducing to FOL* bounded satisfiability 2. Determine FOL* bounded satisfiability by incremental approximation III. Evaluation IV. Conclusion

11. What is FOL*? First-order Logic with quantifiers over relational objects Relational Object Signature Write: loc : Nat value: Int time: Nat Ext:Bool Read: loc : Nat value: Int time: Nat Ext: Bool background theory: LIA R1: Every value written must be eventually read within 100 seconds. R1 = ? ????? ???, ?????, ???? ?:???? ???, ?????, ???? ?.??? = ?.??? ?.????? = ?.????? ?.???? < ?.???? ?.???? + ??? 11

12. MFOTL to FOL* ??. (????? ?,? 0,100 (???? ?,? ) Please check our paper ?:????? ?????1 (??? = 2,????? = 8,???? = 0,??? = ) ?????2 (??? = 1,????? = 10,???? = 0,??? = ) ????1(??? = 2,????? = 8,???? = 100,??? = ) ?:???? ( ?.???? ?.???? + 100 ) ?.??? = ?.??? ?.??? = ?.??? ?.???? ) ????2 (??? = 1,????? = 10,???? = 100,??? = ) ????3 (??? = 2,????? = 8,???? = 200,??? = ) 12

13. Outline I. Problem: Bounded MFOTL satisfiability II. Approach: MFOTL bounded satisfiability checking 1. Reducing to FOL* bounded Satisfiability 2. Determine FOL* bounded Satisfiability by incremental approximation III. Evaluation IV. Conclusion

14. FOL* Bounded Satisfiability Satisfiable? Domain D How to find the domain? ? ?:?????.? ? ,? = (??????.??? ? ??????) ??????.??? ? ?????? read1 write1 read2 write2 read3 write3 Ground FOL* formula ? ? ?:????.? ? ,? = ?????.??? ? ????? r????.??? ? ????? FOL* formula ? is k-bounded satisfiable If and only if there exists a domain ? containing at most k relational objects such that the grounded formula ? ?,? is satisfiable 14

15. Bounded Satisfiability: Naive Approach Problem 1: Grounded formula too large, expansive to check Try the largest domain with k relational object? Domain D read1 write1 K read2 write2 bounded- UNSAT read3 write3 SAT ?(?,?) Ground UNSAT FOL* formula ? Problem 2: Cannot prove ? is UNSAT (unbounded) 15

16. Our Approach: Incremental Approximation Stopping condition, please check our paper UNSAT UNSAT FOL* formula ? 1 K Bounded- UNSAT Over-appr(?,?) SAT 3 Ground Domain Expansion UNSAT 2 Under-appr(?,?) Current Domain D (Under-approx.) New Domain D SAT SAT 16

17. Over-approximation OVER ?:????.? ? ,? = (?????.??? ? ?????) ?????.??? ?(?????) Domain D read1 ?????not included read2 Over- New approximation Instantiation OVER ?:????.? ? ,? = ?????.??? ?(?????) FOL* formula ? Domain D read1 read3 read2 17

18. Under-approximation ? ?,? is equivalent to ?????(?,?) Domain D OVER ?,? read1 read2 Under- Every instantiated relational object is equivalent to some object in ?. approximation FOL* formula ? ????? ????? ????? ????? ????? ????? ????? ????? Domain D read4 read1 read3 read2 18

19. Domain Expansion Expansion goal: Identify the causes of UNSAT and fix them Under-approximation is UNSAT OVER ?,? ??? ??????,? ??? ??????,? ??? ?????,? Over-approximation is SAT OVER ?,? Find a Correction set E.g., ??? ??????,? ,??? ??????,? Can be fixed by dropping constraints Weakened under-approximation is SAT OVER ?,? ??? ?????,? Relational objects to be included to the domain. E.g.,??????and ?????? 19

20. Domain Expansion A* search If solution optimality and termination guarantee is required, Compute Minimum correction set (MCS) over all objects MaxRes: Computing MSC by iteratively analyzing UNSAT cores and weaking assumptions Greedy Best-first Search. More performant If solution optimality is not necessary, Compute Minimum correction set (MCS) over only instantiated objects [3] Maximum Satisfiability Using Core-Guided MaxSAT Resolution. Narodytska, N., Bacchus, F. AAAI 14 20

21. Beyond Domain Approximation UNSAT UNSAT FOL* formula ? 1 K Bounded- UNSAT Over-appr(?,?) SAT We also over- approximate and lazily refine ? 3 Ground Domain Expansion UNSAT 2 Under-appr(?,?) Current Domain D (Under-approx.) New Domain D SAT SAT 21

22. LEGOS LEGOS: MFOTL Bounded Satisfiability Checker LEGOS LEGOS Python API 3000 lines of code PySMT [4] Z3 [5] [4] Pysmt: a solver-agnostic library for fast prototyping of smt-based algorithm. Marco Gario and Andrea Micheli. SMT Workshop 2015 [5]An efficient SMT solver. Leonardo Mendon a de Moura and Nikolaj S. Bj rner. TACAS 2008 22

23. Case-studies Data/ time constraints (PBC, BST, PHIM, CF@H) Complex data constraints (PHIM, CF@H) 23

24. Efficiency of LEGOS with/without Optimality Configurations LEGOS output: UNSAT (U) b-UNSAT (b-U) volume solution (N) nop: no optimal guarantee op: optimal guarantee 24

25. Efficiency of LEGOS with/without Optimality PHIM requirements and legal properties (e.g., ph3) 25

26. Efficiency of LEGOS with/without Optimality 26

27. Efficiency of IBS with/without Optimality 13.80|1905.4 30|29 20.25|682.22 32|29 20.96|1035.87 2.40|778.36 3.54|371.65 5.63|57.3 4.54|65.59 0.48|0.54 27

28. Conclusion Contributions MFOTL bounded satisfiability Decision procedure for MFOTL bounded satisfiability Reducing to FOL* bounded satisfiability Determining FOL* bounded satisfiability via incremental approximation Future work Improve expressiveness (e.g., aggregations) Connect MFOTL and FOL* to front-end DSL Certify UNSAT and bounded UNSAT

29. Thank you LEGOS nick.feng@mail.utoronto.ca PAPER LEGOS checker + Artifacts