Systematic approach to uncover GUI logic flaws

• US 8,156,559 B2
• Filed: 11/30/2006
• Issued: 04/10/2012
• Est. Priority Date: 11/30/2006
• Status: Active Grant

• Current Assignee: Microsoft Technology Licensing LLC (Microsoft Corporation), University of Illinois
• Original Assignee: Microsoft Corporation
• Inventors: Chen, Shuo, Meseguer, Jose, Sasse, Ralf, Wang, Jiahe Helen, Wang, Yi-Min
• Primary Examiner(s): Arani, Taghi
• Assistant Examiner(s): HERZOG, MADHURI R
• Application Number:
  US11/565,426
• Publication Number:
  US 20080134338A1
• Time in Patent Office: 1,958 Days
• Field of Search: 726 22- 25, 717134-135, 717140-144, 713/187
• US Class Current: 726/25
• 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 of uncovering logic flaws of a graphical user interface (GUI) comprising:

mapping a visual invariant that is seen by a user, to a program invariant comprising Boolean flags associated with an execution context, the mapping based on a browser'"'"'s logic for mouse handling and page loading;

discovering inputs to GUI logic that include user actions and execution context to cause the program invariant to be violated; and

identifying the logic flaws of the GUI based on the inputs that cause the program invariant to be violated;

wherein the visual invariant relates consistency between a user'"'"'s visual perception and a browser state; and

wherein the discovering is used as a guidance for constructing real visual spoofing attacks.

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 1, wherein the program invariant further comprises a Boolean condition that is formally reasoned about.

4. The method of claim 1, wherein the discovering comprises document object trees, active scripts, and user actions that cause the visual invariant to be violated.

5. The method of claim 1, performed as to browser status bar spoofing.

6. The method of claim 1, performed as to browser address bar spoofing.

7. The method of claim 1, further comprising generating an action sequence.

8. The method of claim 7, 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.

9. A computer readable device having computer-executable modules executable by a computing device, comprising:

a reasoning engine that performs steps comprising;

defining a formal model of a graphical user interface (GUI) comprised of a user action sequence, an execution context, and GUI states, the GUI states represented by symbolic expressions indicating how a GUI state is transformed into another GUI state;

mapping one or more visual invariants that are seen by a user to one or more program invariants comprising Boolean flags associated with the GUI states, the mapping based on a browser'"'"'s logic for mouse handling and page loading;

identifying logic flaws of the GUI based on inputs that cause the one or more program invariants to be violated; and

in response to a violation of a particular program invariant of the one or more program invariants, outputting a spoofing scenario based on the user action sequence, the execution context, and the GUI state at the time that the violation occurred;

wherein the one or more visual invariants relate consistency between a user'"'"'s visual perception and a browser state.

10. The computer readable device of claim 9, wherein program logic of the system is derived from browser source code.

11. The computer readable device of claim 9, wherein the spoofing scenario is mapped to a real world subsystem through an attack construction.

12. The computer readable device of claim 11, further comprising constructing a page based on the spoofing scenario output from the reasoning engine.