Systematic approach to uncover GUI logic flaws
View Patent ↗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.
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.