Database Management in Computer Science

Dr. Xiang Fu Assistant Professor Hofstra University Department of Computer Science

Introduction Path Transducer Model Relational Constraint Call Sequence Synthesis Detecting Workflow Attack Related Work and Conclusion

Databases Databases Web Server Web Server

Traditionally, SQLUnit Manual Reverse Inference of DB State Given Query Generate Initial DB Instance Our Problem: Synthesis Problem Given Database State Synthesize Call Sequence SQLUnit & DBUnit DBUnit Manual Test Case Design Query & Expected Result Expected Result Database State Call Sequence of Servlets

White-box Analysis (1) Interface Extraction Path Transducers (2) Coverage Goal Extraction (3) Call Sequence Generation Adaptation Discover Workflow Attacks

Servlet Path Transducers Relational Transducer that Models One Execution Path Path Condition Side Effects to DB Servlet

Relational Data Schema Input Domain Finite Set of Session Variables Boolean Combination of Terms Equality v = v + 1 Satisfiability Check )) ( ( SAT ' ' 2 1 T a =

Selection = ( ) 1 2 2 Projection ( ) 1 Cross Product 2 Union 1 2 Difference 1 2

SimpleScarf Login.php ShowSessions.php GenOptions.php AddMember.php InsertSession.php

U Users S Sessions int sid vchar uname vchar pwd vchar sname M Members int sid vchar uname

Check Valid Session Var #uname Select Session Info No Side Effects #uname

User Specify New Session Name $S Update Relation Sessions $SI I Sessions

Takes Two Parameters $u $s Add Membership Info $uA A: User Name $sA A: Session Name

Add User: One of Many Functions Available Takes Two Parameters $u $p $uG G: User name $pG G: Password Encrypt Password Password Rules Encoded Using String Constraint

Given Two Parameters $u $p When Success, Update Session Variable #u $uL L: user name $pL L: password #u: Session Variable on user name

Key to Synthesis Khurshid sApproach [ASE 08] Translate to Alloy

Post Image Transition System

Join of Session and Membership Select Session Name s1 Find users in paper session s1 but not in s2 Project to uname Goal: Find DB Instance Satisfies Satisfies query

Vars Vars Clauses Clauses Trans_Time Trans_Time Solve_Time Solve_Time 4833 7876 829ms 829ms 78ms 78ms

Coverage Goal: Line # 45 List of HTTP Requests CALL Seq Synthesis Algorithm Path Transducers

Knowledge In Advance: (1) Each Path Transducer (Relational Logic) (2) Relations (3) Session Algorithm: Backtrack Each Path Transducer Transition System Relations being Modified (add, drop, modify) Session Vars Vars being Modified = Pre(H , ) Current Constraint Heuristic to pick to the next servlet: watch the difference between the relations in the current constraints and target constraints. Insertion has priority HTTP Request ( , ) ( , )

Coverage Goal Target Constraint Initial Constraint Path Transducer: Target Constraint: True Initial Constraint: Path Transducer:

Transition Post-Image Standard Existential Quantification M M and #u Next servlet: AddMember #u modified! Compare AddMember or Login Login Initial Constraint Initial Constraint:

1.07 seconds for generating the model by ALLOY

EnterAddr ChargeCC GenReceipt PrintShipping How to Detect Workflow Attack? How to Detect Workflow Attack? (1) Static Analysis for ALL URLS that could be generated by a servlet (2) Modify the Backtrack algorithm for locating an abnormal link not in the ALL_URLs set Database manipulation TAKEN CARE OF.

Proposal of Several Interesting Directions Extraction of Path Transducer Model Solving Relational Constraints Call Sequence Synthesis Algorithm Extension for Detecting Workflow Attacks Future Directions Implementation

Interface Extraction [Halfond FSE07], [Halfond FSE 08] Relational Transducer [Abiteboul JCSS00] Query Aware Relational Constraint Solving [Binnig ICDE07, Khalek ICSE08] Session Based Testing of Web App [Elbaum TSE05, Sampath ASE05, Sprenkle FSE05]