Ambient calculus-based modal logics for mobile ambients

• US 7,721,335 B2
• Filed: 08/30/2004
• Issued: 05/18/2010
• Est. Priority Date: 03/18/1999
• Status: Active Grant

• Current Assignee: Microsoft Technology Licensing LLC (Microsoft Corporation)
• Original Assignee: Microsoft Corporation
• Inventors: Ghelli, Giorgio, Cardelli, Luca, Gordon, Andrew D.
• Primary Examiner(s): Moazzami; Nasser
• Assistant Examiner(s): Louie; Oscar A
• Application Number:
  US10/929,742
• Publication Number:
  US 20050043932A1
• Time in Patent Office: 2,087 Days
• Field of Search: 726 1- 4, 726/16, 726/17, 726/21, 726/22, 726/25, 726/27, 726/31, 713/189, 380/59
• US Class Current: 726/25
• CPC Class Codes: G06F 21/50 Monitoring users, programs or devices to maintain the integrity of platforms, e.g. of processors, firmware or operating systems
• CPC Class Codes: G06F 21/51 at application loading time, e.g. accepting, rejecting, starting or inhibiting executable software based on integrity or source reliability

Abstract

Ambient calculus-based modal logics for mobile ambients are disclosed. Formal analysis mechanisms or frameworks with which mobile ambients can be described, and within which policies such as security policies can be tested against those ambients, are disclosed. In one embodiment, a computer-implemented method receives at least one container, where each container has at least one process. The method applies the containers, including their processes, against a predetermined modal logic. The modal logic is based on ambient calculus, and provides for spatial relationships among the processes of the containers. The containers and their processes are output, as applied against the logic.

Claims

1. A computer-implemented method performed by a processor executing computer-executable instructions stored on a computer-readable media storage, the method of describing and analyzing mobile containers, comprising:

receiving a configuration of at least one container, the container having at least one process, wherein the configuration represents a mobile computing environment and defines a policy;

providing an ambient calculus-based representation of the at least one container and the at least one process;

matching a syntactic structure of expressions in ambient calculus to a structure of the at least one container and the at least one process to process equivalence;

deriving a number of logical inference rules for propositional logic, rules for modal operators, rules for locations, and rules for process compositions;

testing the ambient calculus-based representation of the at least one container and the at least one process with an ambient calculus-based representation of the policy;

instructing the at least one container how to behave based at least in part on situations, the situations include the policy instructing the at least one container and the at least one process to move in and to move out into a parent container, the policy executing on the at least one container, and a replicated instruction is executed on the at least one process; and

outputting a test result that indicates whether the ambient calculus-based representation of the at least one container and the at least one process satisfies the ambient calculus-based representation of the policy.

2. The method of claim 1, the at least one container is a mobile ambient.

3. The method of claim 1, the at least one process is a thread or an agent.

4. The method of claim 1, the ambient calculus provides for spatial relationships among the processes.

5. The method of claim 1, the ambient calculus provides for one or more of a structural congruence relation;

reduction semantics;

logical formulae;

derived connectives;

sequents;

logical inference rules;

quantales; and

intuitionistic linear logic.

6. The method of claim 5, the logical formulae includes one or more of true, negation, disjunction, inaction, location, composition, universal quantification over names, sometime modality, somewhere modality, location adjunct, and composition adjunct.

7. The method of claim 5, the derived connectives include one or more of false, conjunction, implication, logical equivalence, decomposition, every component satisfaction, some component satisfaction, existential quantification over names, every time modality, everywhere modality, and unsatisfiability.

8. The method of claim 1, the policy is one of a security policy and a formula.

9. The method of claim 8, the security policy, and the formula defines whether the container can move from one parent container to another parent container.

10. The method of claim 1, further comprising allowing the at least one container to move out of or into a parent container or to replicate when the test result indicates that the ambient calculus-based representation of the at least one container and the at least one process satisfies the ambient calculus-based representation of the policy.

11. The method of claim 1, the policy defines a scope of a behavior associated with the at least one container.

12. The method of claim 11, the behavior includes at least one of the at least one process moving out of the at least one container, a second process moving into the at least one container, and the at least one process duplicating itself.

13. The method of claim 1, the outputting of the test result is analyzed by a program, displayed on a display device, printed to a printer, and/or stored in a storage device.

14. A computing system that executes the method of claim 1.

15. A system that employs ambient calculus to test mobile ambients, comprising:

a memory;

a processor coupled to the memory;

the processor coupled to a transformation component, an analysis component, and an output component;

the transformation component that makes assertions about containment and contiguity of a plurality of ambients;

the transformation component matches a syntactic structure of expressions in an ambient calculus-based modal logic to a structure of the plurality of ambients and associated processes, and represents the plurality of ambients and the associated processes in the ambient calculus-based modal logic;

the transformation component that derives a number of logical inference rules for propositional logic, rules for modal operators, rules for locations, and rules for process compositions;

the analysis component that determines whether an ambient of the plurality of ambients satisfies a policy by testing a representation of the ambient with an ambient calculus-based modal logic representation of the policy;

wherein instructions on how the at least one container behaves based at least in part on situations, the situations include the policy instructing the at least one container and the at least one process to move in and to move out into a parent container, the policy executing on the at least one container, and a replicated instruction is executed on the at least one process;

the output component that provides a result of the analysis, the result being utilized to effectuate an action associated with the ambient.

16. The system of claim 15, the ambient calculus provides for spatial relationships among the associated processes.

17. The system of claim 15, the policy is one of a security policy and a formula that defines whether the ambient and/or at least one of the associated processes can move into or out of another ambient.

18. The system of claim 15, the action is a move or a replication.

19. The system of claim 15, the result is analyzed by software running on a computer, displayed on a monitor, printed, and/or stored for further processing at a later time.

20. The system of claim 15, the ambient calculus provides for one or more of a structural congruence relation;

reduction semantics;

logical formulae;

derived connectives;

sequents;

logical inference rules;

quantales; and

intuitionistic linear logic.

21. The system of claim 20, the logical formulae includes one or more of true, negation, disjunction, inaction, location, composition, universal quantification over names, sometime modality, somewhere modality, location adjunct, and composition adjunct.

22. The system of claim 20, the derived connectives include one or more of false, conjunction, implication, logical equivalence, decomposition, every component satisfaction, some component satisfaction, existential quantification over names, every time modality, everywhere modality, and unsatisfiability.

23. The system of claim 15 is stored on a computer-readable medium for distribution, installation and execution on a computer.

24. A computer-implemented method having computer instructions that are executable on a processor, the method, comprising:

receiving a first ambient calculus based representation of a plurality of ambient that defines a policy or a formula, wherein the first representation is based on at least a predetermined logic, a configuration of the predetermined logic represented by at least one container and at least one process;

receiving a second ambient calculus based representation of a plurality of ambients, wherein the second representation is of the configuration of a mobile computing environment and defines the policy;

comparing the second representation and the first representation within the predetermined logic;

determining whether the second representation satisfies the policy or the formula of the first representation, based on the comparison;

testing the second representation against the first representation based on at least in part on the predetermined logic;

providing a result that indicates whether the second representation satisfies the first representation.

instructing the at least one container how to behave based at least in part on situations, the situations include the policy instructing the at least one container and the at least one process to move in and to move out into a parent container, the policy executing on the at least one container, and a replicated instruction is executed on the at least one process; and

outputting a test result that indicates whether the second representation of the at least one container and the at least one process satisfies the first representation of the policy.

25. A computer readable medium storing computer executable components that facilitate an analysis of mobile ambients, comprising:

a first component that makes assertions about containment and contiguity of a plurality of ambients;

the first component that matches a syntactic structure of expressions in an ambient calculus-based modal logic to a structure of the plurality of ambients and associated processes, and represents the plurality of ambients, the associated processes and a policy in ambient calculus;

the first component that derives a number of logical inference rules for propositional logic, rules for modal operators, rules for locations, and rules for process compositions;

a second component that compares the representations;

the second component that tests the representations against each other;

instructing at least one container how to behave based at least in part on situations, the situations include the policy instructing the at least one container and at least one process to move in and to move out into a parent container, the policy executing on the at least one container, and a replicated instruction is executed on the at least one process; and

outputting a test result that indicates whether the plurality of ambients satisfies the ambient calculus-based representation of the policy.

26. The computer readable medium of claim 25, wherein the ambient calculus provides for spatial relationships among the associated processes.

27. The computer readable medium of claim 26, wherein the ambient calculus provides for one or more of a structural congruence relation between processes;

reduction semantics;

logical formulae;

derived connectives;

sequents;

logical inference rules;

quantales; and

intuitionistic linear logic.

28. The computer readable medium of claim 27, wherein the logical formulae includes one or more of true, negation, disjunction, inaction, location, composition, universal quantification over names, sometime modality, somewhere modality, location adjunct, and composition adjunct.

29. The computer readable medium of claim 27, wherein the derived connectives include one or more of false, conjunction, implication, logical equivalence, decomposition, every component satisfaction, some component satisfaction, existential quantification over names, everytime modality, everywhere modality, and unsatisfiability.

30. A system that facilitates describing and analyzing mobile ambients, comprising:

means for representing a received ambient and associated process in ambient calculus;

means for matching a syntactic structure of expressions in the ambient calculus to a structure of at least one container and the associated process to process equivalence;

means for deriving a number of logical inference rules for propositional logic, rules for modal operators, rules for locations, and rules for process compositions;

means for testing the ambient calculus representation of the ambient and the associated process with an ambient calculus representation of a policy;

means for instructing at least one container how to behave based at least in part on situations, the situations include the policy instructing the at least one container and the associated process to move in and to move out into a parent container, the policy executing on the at least one container, and a replicated instruction is executed on the associated process; and

means for determining whether the ambient satisfies the policy, based on the testing; and

means for providing a result of the test that effectuates an action of the ambient and/or the associated process.