Systematic Approach to Uncover Visual Ambiguity Vulnerabilities

• US 20080133976A1
• Filed: 06/25/2007
• Published: 06/05/2008
• Est. Priority Date: 11/30/2006
• Status: Active Grant

• Current Assignee: Microsoft Technology Licensing LLC (Microsoft Corporation)
• Original Assignee: Microsoft Corporation
• Inventors: Wang, Yi-Min, Wang, Jiahe Helen, Chen, Shuo, Sasse, Ralf
• Granted Patent: US 8,539,585 B2
• Time in Patent Office: Days
• US Class Current: 714/38
• CPC Class Codes: G06F 11/3608 using formal methods, e.g. model checking, abstract interpretation theorem proving G06N5/013
• CPC Class Codes: G06F 21/577 Assessing vulnerabilities and evaluating computer system security
• CPC Class Codes: G06F 21/83 input devices, e.g. keyboards, mice or controllers thereof

Abstract

To achieve end-to-end security, traditional machine-to-machine security measures are insufficient if the integrity of the graphical user interface (GUI) is compromised. GUI logic flaws are a category of software vulnerabilities that result from logic flaws in GUI implementation. The invention described here is a technology for uncovering these flaws using a systematic reasoning approach. Major steps in the technology include: (1) mapping a visual invariant to a program invariant; (2) formally modeling the program logic, the user actions and the execution context, and systematically exploring the possibilities of violations of the program invariant; (3) finding real spoofing attacks based on the exploration.

Claims

1. A method comprising:

mapping a visual invariant to a program invariant; and

discovering inputs to GUI logic that includes a user actions and an execution context to cause the program invariant to be violated.

2. The method of claim 1 using formal methods to systematically explore the program state space, wherein the formal methods comprise rewriting logic framework, theorem provers, and model checkers.

3. The method of claim 2, wherein a prototype has been implemented using the rewriting logic framework.

4. The method of claim 1, wherein the program invariant is a Boolean condition that can be formally reasoned about.

5. The method of claim 1, wherein the visual invariant is an informal definition about the consistency between a user'"'"'s visual perception and a browser state.

18. The method of claim 1, wherein the program invariant is specified in a search operation that explores the action sequence and the execution contexts to discover spoofs, wherein the action sequences and the execution contexts are canonical.

6. An reasoning engine comprising:

a formal model of a system comprised of a user action sequence, an execution context, and system state; and

one or more program invariants, wherein a spoofing scenario is output if a program invariant is violated based on the user action sequence, the execution context, and the system state.

7. The reasoning engine of claim 6 is implemented to model the status bar correctness.

8. The reasoning engine of claim 6 is implemented to model the address bar correctness.

9. The status bar model in claim 7, wherein the user action sequence is represented as a list of actions, which is a First-In-First-Out (FIFO) queue.

10. The status bar model in claim 7, wherein the execution context (i.e., the HTML tree) is represented as a multi-set of HTML elements. These elements have certain structural attributes to maintain the tree structure and association relationships with other elements.

11. The status bar model in claim 7, wherein the system state includes the URL displayed on the status bar and the URL memories by the user.

12. The status bar model in claim 7, wherein the execution of an action is modeled by removing the first action from the action list, and changing the system states according to the semantics of the action.

13. The address bar model in claim 8, wherein the user action sequence is represented by multiple “

new-page loading”

, “

history-travelling” and

“

new-window opening”

actions in a specific order. The actions are represented in an FIFO queue called the “

action list”

.

14. The address bar model in claim 8, wherein the system states include the address bar, the primary frame, a set of non-primary frames, the View structure, the pending markups and the current markups, which are represented as a multi-set of the system'"'"'s attributes.

15. The address bar model in claim 8, each action invokes a series of browser functions, which are represented in an FIFO queue called the “

function list”

.

16. The address bar model in claim 8, handling an action is modeled by removing the action from the beginning of the action list, and appending a corresponding handler function to the function list.

17. The address bar model in claim 8, posting an action is modeled by appending the action to the action list.

19. The reasoning engine of claim 6, wherein the program logic of the system is derived from browser source code.

20. The reasoning engine of claim 6, wherein the spoofing scenario is mapped to a real world subsystem through the attack construction.

21. The attack construction of claim 20, further comprising constructing a page based on the spoofing scenario output from the reasoning engine.

22. The reasoning engine of claim 6, wherein optimization techniques can be applied on the modeled expressed in the writing logic framework. In particular, rules expressing equality relations can be replaced by equations to greatly reduce the search space without loss of non-trivial scenarios.

23. The reasoning engine of claim 6, wherein the canonicalization of the user action sequence and the execution context is critical to reduce the input space.