Ambient calculus-based modal logics for mobile ambients

• US 20050043932A1
• Filed: 08/30/2004
• Published: 02/24/2005
• Est. Priority Date: 03/18/1999
• Status: Active Grant

• Current Assignee: Microsoft Technology Licensing LLC (Microsoft Corporation)
• Original Assignee: Microsoft Corporation
• Inventors: Gordon, Andrew D., Ghelli, Giorgio, Cardelli, Luca
• Granted Patent: US 7,721,335 B2
• Time in Patent Office: Days
• US Class Current: 703/1
• 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 for describing and analyzing mobile containers, comprising:

receiving at least one container, the container has at least one process;

testing an ambient calculus-based representation of the at least one container and the at least one process with an ambient calculus-based representation of a policy; 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, further comprising representing the at least one container and the at least one process in ambient calculus.

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

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

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

6. 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.

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

8. The method of claim 6, the derived connectives include on 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.

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

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

11. The method of claim 1, further comprising allowing the 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.

12. The method of claim 1, the policy defines a scope of a behavior associated with the container.

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

14. The method of claim 1 is a program that executes from a computer-readable medium by a processor.

15. The method of claim 14, the computer-readable medium is one of a floppy disk and CD-ROM.

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

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

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

a transformation component that represents an ambient and associated processes in an ambient calculus-based modal logic;

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

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

19. The system of claim 18, the ambient calculus provides for spatial relationships among the processes.

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

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

22. The system of claim 18, 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.

23. The system of claim 18, 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.

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

25. The system of claim 23, the derived connectives include on 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.

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

27. A computer-implemented method, comprising:

receiving a first ambient calculus based representation that defines a formula;

receiving a second ambient calculus based representation of a plurality of ambients;

comparing the second representation and the first representation;

determining whether the second representation satisfies the first representation, based on the comparison; and

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

28. A data packet transmitted between two or more computer components that facilitates mobile ambient analysis, comprising:

an ambient represented in ambient calculus-based modal logic, the representation is analyzed against an ambient calculus-based policy, the analysis determines whether the ambient satisfies the policy.

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

a component that represents an ambient and a policy in ambient calculus; and

a component that compares the representations and outputs a result that indicates whether the ambient satisfies the policy.

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 testing the ambient calculus representation of the ambient and associated process with an ambient calculus representation of a policy;

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.