Concurrent Interpretations of Authorization Logic

Explore the concepts of authorization logic through discussions on policy enforcement, permissions, logical implications, and security theorems in the context of a scenario involving Alice, UdS Students, and printing permissions.

• Authorization Logic
• Policy Enforcement
• Permissions
• Logical Implications
• Security Theorems

franky Follow

Uploaded on Jul 10, 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. Concurrent Interpretations of Authorization Logic Andrew K. Hirsch Boston Computing Club March 13 2021 1

2. Is Alice a UdS Is Alice allowed to print? student? Alice is a UdS Student I want to print a document Policy: UdS Students may print Alice is a UdS Student

3. Questions about authorization: thentication How do we state authorization policies? How do we reason about authorization policies? How do we enforce authorization policies? Who is who? Main focus of today s talk Touch on if time Who may do what? thorization What do we record? dit

4. Permissions Principals System Components Users Software Modules Machines Alice may print Policies Beliefs Policy: UdS Students may print Alice is a UdS Student Wrong Beliefs Compromised

5. Does this policy subsume that? Under what circumstances may Alice e.g., print? Why is something (not) allowed? Logical Implications Any principal which is a UdS Student may print. MayPrint(?) ? Prin, isStudent ? Policy: UdS Students may print Not all relations are permissions Permissions are relations

6. Printer says isStudent(Alice) Printer says UdS speaks for Printer Alice is a UdS Student UdS says isStudent(Alice) Bob says isStudent(Alice)

7. Q: May Alice print? Assuming things on the left are true, prove the thing on the right Policy: UdS Students may print MayPrint(Alice) , May Alice print in May Alice print under this policy? this model and under this policy? ? Prin, isStudent ? MayPrint(?) System Model

8. isStudent(Alice) MayPrint(Alice) Policy: UdS Students Noninterference may print , , Only those you trust can hurt you Main security theorem for authorization logic isStudent(Alice) Policy: UdS Students may print Speaks For , ,

9. If everything up here is true A B D E ? Logical Formula Then so is everything down here Need rules for proofs Set of Logical Formulae

10. ,?,? ? ,? & ? ? ? ? ? ? ? & ? &-L &-R axiom You can use an assumption of ?&?by using an assumption of ? and an assumption of ? You can prove ?& ?by proving ?and ? You can prove ? by assuming it

11. ? ? axiom ,?,? ? ,? & ? ? &-L ? ? ? & ? &-R ? ?,? ? ?,? axiom axiom ?,? ? ?,? ? &-R ?,? ? & ? &-L ? & ? ? & ?

12. isStudent(Alice) MayPrint(Alice)

13. Principals are Reasoners Principals can reason from their beliefs to derive new beliefs ?,?, ? ? ? ? , ,

14. Says Reflection Principals know what they believe. ? ?

15. Says Join Principals are right about what they believe. ? ?

16. Counit does NOT hold Principals may believe untrue things ? ? This rule is common in logics of knowledge, rather than belief

17. Should Unit Hold? Principals believe all true things Yes No Extremely Influential ? ?

18. Confidentiality (2020) Unit can leak secrets I owe $100 I owe $100 Formal treatment of confidentiality in authorization

19. Distribution (2013) Unit can break distributivity CPUState(3) CPUState(3) Argument about distribution made informally

20. The Propositions-as-Types Principle Logic Computation

21. The Propositions-as-Types Principle Logic Propositions Computation Types

22. The Propositions-as-Types Principle Logic Propositions Proofs Computation Types Programs

23. The Propositions-as-Types Principle Logic Propositions Proofs Assumptions Computation Types Programs Inputs

24. The Propositions-as-Types Principle Logic Propositions Proofs Assumptions Conclusions Computation Types Programs Inputs Outputs

25. The Curry-Howard Isomorphism The Curry-Howard Correspondance Haskell Curry William Howard Andrej Kolmogorov LEJ Brouwer Arend Heyting The Brouwer- Heyting- Kolmogorov Interpretation Picture of William Howard from UIC. All others from Wikimedia Commons.

26. ? ? ? ? Assumptions are variables var ,? ?,? ? ? ? ,? ? & ? let (?,?) ? in Match ? ? Evidence for ?&? is a pair of evidence for ? and ? ?1 ? ?2 ? ?1,?2 ? & ? Pair

27. ? ? ? ?,? ? ? ? ? ?,? ? ? ?,? ? ? ? ? ?,? ? ? ? ? ?,? ? ?,? ? & ? ? & ? let ?,? ? in ?,? ? & ?

28. The Propositions-as-Types Principle Logic Propositions Proofs Assumptions Conclusions Principals Computation Types Programs Inputs Outputs

29. The Propositions-as-Types Principle Logic Propositions Proofs Assumptions Conclusions Principals Trust Computation Types Programs Inputs Outputs

30. The Propositions-as-Types Principle Logic Propositions Proofs Assumptions Conclusions Principals Trust Communication Computation Types Programs Inputs Outputs

31. The Propositions-as-Types Principle Logic Propositions Proofs Assumptions Conclusions Principals Computation Types Programs Inputs Outputs Processes (Computers, threads, ) Trust Communication

32. The Propositions-as-Types Principle Logic Propositions Proofs Assumptions Conclusions Principals Computation Types Programs Inputs Outputs Processes (Computers, threads, ) Channels Trust Communication

33. The Propositions-as-Types Principle Logic Propositions Proofs Assumptions Conclusions Principals Computation Types Programs Inputs Outputs Processes (Computers, threads, ) Channels Message-Passing Trust Communication

34. Need a programming paradigm with Processes Message-Passing Communication A Top-Down Point of View I.e., not a separate program for each process

35. ? .? .?

36. ; .? .? By treating these programs as equivalent, we can reason about concurrency.

37. .? Are Choreographies Good Enough? Untyped (or Session Typed) Stateful No interpretation for common logical connectives (e.g., implication) No channels No interpretation for beliefs about beliefs Receive from Alice Send ? to Bob

38. Functional Choreographies Ongoing joint work with Deepak Garg

39. .? ; .? .? .? now refers to ? Whole program computes a value on .?

40. s view of ? ? .? ? .?

41. .?refers to s ? (rec ? .? .?) ? Functions of local values Can recursively call ? Not bound in any process (rec ? ? .?1) ?2 Functions of global values ? refers to ?2 Can recursively call ?

42. .? ?, ? ? (rec ? .? .?) .? ? local

43. (rec ? .? .?) ? Are Choreographies Good Enough? Untyped (or Session Typed) Stateful No interpretation for common logical connectives (e.g., implication) No channels No interpretation for beliefs about beliefs s view of C Dummy value (rec ? ? . ? ) () (rec ? ? . ? ) ?

44. Extending Functional Choreographies Much more speculative portion of the talk Ongoing joint work with Hannah Gommerstadt, Alex Kavvos, Daniel Gratzer, Lars Birkedal, and Deepak Garg

45. speaks for (rec ? ? .?) Are Choreographies Good Enough? Untyped (or Session Typed) Stateful No interpretation for common logical connectives (e.g., implication) No channels No interpretation for beliefs about beliefs Functions of Channels Values as a language parameter Network Topology Computes to (rec ? Session-Typed Higher-Order Processes .?1) ?2 Functions of Principals How to compile?

46. Authorization Logic Functional Choreographies ? Topology ? Are Choreographies Good Enough? Untyped (or Session Typed) Stateful No interpretation for common logical connectives (e.g., implication) No channels No interpretation for beliefs about beliefs speaks for Computation Processes ? ? Network Simulation

47. Distribution Unit can break distributivity CPUState(3) CPUState(3) Need a computation that runs on but doesn t run on s simulation

48. Questions about authorization: How do we state authorization policies? How do we reason about authorization policies? How do we enforce authorization policies? Prove programs follow policies using Propositions-as-types

49. Write program in typed functional language Requires dependent types Same language Compatible Write policy as a type Prove your policy, thereby showing that it is followed Enforcement Neutral

50. Thank You Authorization policies can be reasoned about with logic Rules for this logic are not obvious Building concurrent interpretations helps us understand what rules are desirable and can help us build verification tools as well