Yuri Gurevich (Microsoft Research)
Cloud security and the logic of infons
Abstract: In software industry engineers often do formal logic even though they may not realize that. Security policy is one of those fields where engineers do logic. The security policy of a large organization consists of great many rules. You want to throw in a few more rules. Are you sure that they do not contradict the current policy? Is the current policy is consistent? Is the meaning of the rules well defined? Are there unintended ambiguities? Is your policy in compliance with government regulations? The relentless move to the cloud aggravates these and related problems. A few logic-based languages arose to deal with these problems. As a rule they presume a central logic engine. Our policy language, called DKAL, goes beyond that. It formalizes not only logic but also communication which facilitates reasoning about interacting policies. But it is the logic of DKAL - infon logic - that is main topic of the lecture. Infons are declarative sentences viewed as pieces of information. One doesn't ask whether a given infon is true or false; it may be neither. A better question is who knows that infon. We will describe the logic if infons. In particular we will present so-called primal infon logic, very efficient and yet sufficiently expressive for many authorization purposes. The derivation problem for primal infon logic is solvable in linear time. |
|
