Parameter tampering attacks are dangerous to a web application whose server performs weaker data sanitization than its client. This paper presents TamperProof, a methodology and tool that offers a novel and efficient mechanism to protect Web applications from parameter tampering attacks. TamperProof is an online defense deployed in a trusted environment between the client and server and requires no access to, or knowledge of, the server side codebase, making it effective for both new and legacy applications. The paper reports on experiments that demonstrate TamperProof's power in efficiently preventing all known parameter tampering vulnerabilities on ten different applications.

The current practice of web application development treats the client and server components of the application as two separate but interacting pieces of software. Each component is written independently, usually in distinct programming languages and development platforms --- a process known to be prone to errors when the client and server share application logic. When the client and server are out of sync, an impedance mismatch occurs, often leading to software vulnerabilities as demonstrated by recent work on parameter tampering. This paper outlines the groundwork for a new software development approach, WAVES, where developers author the server-side application logic and rely on tools to automatically synthesize the corresponding client-side application logic. WAVES employs program analysis techniques to extract a logical specication from the server, from which it synthesizes client code. WAVES also synthesizes interactive client interfaces that include asynchronous callbacks whose performance and coverage rival that of manually written clients while ensuring no new security vulnerabilities are introduced. The effectiveness of WAVES is demonstrated and evaluated on three real-world web applications.

The current practice of web application development treats the client and server components of the application as two separate but interacting pieces of software. Each component is written independently, usually in distinct programming languages and development platforms --- a process known to be prone to errors when the client and server share application logic. When the client and server are out of sync, an impedance mismatch occurs, often leading to software vulnerabilities as demonstrated by recent work on parameter tampering. This paper outlines the groundwork for a new software development approach, WAVES, where developers author the server-side application logic and rely on tools to automatically synthesize the corresponding client-side application logic. WAVES employs program analysis techniques to extract a logical specication from the server, from which it synthesizes client code. WAVES also synthesizes interactive client interfaces that include asynchronous callbacks whose performance and coverage rival that of manually written clients while ensuring no new security vulnerabilities are introduced. The effectiveness of WAVES is demonstrated and evaluated on three real-world web applications.

Access control schemes come in all shapes and sizes, which makes choosing the right one for a particular application a challenge. Yet today's techniques for comparing access control schemes completely ignore the setting in which the scheme is to be deployed. In this paper, we present a formal framework for comparing access control schemes with respect to a particular application. The analyst's main task is to evaluate an access control scheme in terms of how well it implements a given access control workload (a formalism that we introduce to represent an application's access control needs). One implementation is better than another if it has stronger security guarantees, and in this paper we introduce several such guarantees: correctness, homomorphism, AC-preservation, safety, administration-preservation, and compatibility. The scheme that admits the implementation with the strongest guarantees is deemed the best fit for the application. We demonstrate the use of our framework by evaluating two workloads on ten different access control schemes.

Weblog is a declarative language for web application development designed to automatically eliminate several security vulnerabilities common to today's web applications. In this paper, we introduce Weblog, detail the security vulnerabilities it eliminates, and discuss how those vulnerabilities are eliminated. We then evaluate Weblog's ability to build and secure real-world applications by comparing traditional implementations of 3 existing small- to medium-size web applications to Weblog implementations.

The current practice of web application development treats the client and server components of the application as two separate but interacting pieces of software. Each component is written independently, usually in distinct programming languages and development platforms--- a process known to be problematic when the client and server must share application logic. When the client and server are out of sync, an impedance mismatch occurs, often leading to software vulnerabilities as demonstrated by recent work on parameter tampering. This paper outlines the groundwork for a new software development approach, WAVES, where developers author the server-side application logic and rely on tools to automatically synthesize the corresponding client-side application logic. WAVES employs program analysis techniques to extract a logical specification from the server and synthesizes client code from that specification. WAVES also synthesizes interactive client interfaces that include asynchronous callbacks whose performance and coverage rival that of manually written clients, while ensuring that no new security vulnerabilities are introduced. We demonstrate and evaluate the effectiveness of WAVES on three real-world web applications.

Access control is an area where one size does not fit all. However, previous work in access control has focused solely on expressiveness as an absolute measure. Thus, we discuss and justify the need for a new type of evaluation framework for access control, one that is application-aware. To this end, we apply previous work in access control evaluation, as well as lessons learned from evaluation frameworks used in other domains. We describe the analysis components required by such a framework, the challenges involved in building it, and our preliminary work in realizing this ambitious goal. We then theorize about other areas within the security domain that display a similar absence of such evaluation tools, and consider ways in which we can adapt our framework to analyze these broader types of security workloads.

Tag-Based Authorization (TBA) is a hybrid access control model that combines the ease of use of extensional access control models with the expressivity of logic-based formalisms. The main limitation of TBA is that it lacks support for policy administration. More precisely, it does not allow policy-writers to specify administrative policies that constrain the tags that users can assign, and to verify the compliance of assigned tags with these policies. In this paper we introduce TBA2 (Tag-Based Authorization & Administration), an extension of TBA that enables policy administration in distributed systems. We show that TBA2 is more expressive than TBA and than two reference administrative models proposed in the literature, namely HRU and ARBAC97.

Parameter tampering attacks are dangerous to a web application whose server fails to replicate the validation of user-supplied data that is performed by the client. Malicious users who circumvent the client can capitalize on the missing server validation. In this paper, we describe WAPTEC, a tool that is designed to automatically identify parameter tampering vulnerabilities and generate exploits by construction to demonstrate those vulnerabilities. WAPTEC involves a new approach to whitebox analysis of the server's code. We tested WAPTEC on six open source applications and found previously unknown vulnerabilities in every single one of them.

Modern web forms interact with the user in real-time by detecting errors and filling-in implied values, which in terms of automated reasoning amounts to SAT solving and theorem proving. This paper presents Plato, a compiler that automatically generates web forms that detect errors and fill-in implied values from declarative web form descriptions. Instead of writing HTML and JavaScript directly, web developers write an ontology in classical logic that describes the relationships between web form fields, and Plato automatically generates HTML to display the form and browser scripts to implement the requisite SAT solving and theorem proving. We discuss Plato's design and implementation and evaluate Plato's performance both analytically and empirically.

Experiments:experiments/padl2011_ontologies.tar.gz Related: [hinrichs2011plato-full] [hinrichs2010automatic]

Logical policy-based access control models are greatly expressive and thus provide the flexibility for administrators to represent a wide variety of authorization policies. Extensional access control models, on the other hand, utilize simple data structures to better enable a less trained and non-administrative workforce to participate in the day-to-day operations of the system. In this paper, we formally study a hybrid approach, tag-based authorization (TBA), which combines the ease of use of extensional systems while still maintaining a meaningful degree of the expressiveness of logical systems. TBA employs an extensional data structure to represent metadata tags associated with subjects and objects, as well as a logical language for defining the access control policy in terms of those tags. We formally define TBA and introduce variants that include tag ontologies and delegation. We evaluate the resulting system by comparing to well-known extensional and logical access control models.

Model checking and runtime verification are pillars of formal verification but for the most part are used independently. In this position paper we argue that the formal verification community would be well-served by developing theory, algorithms, implementations, and applications that combine model checking and runtime verification into a single, seamless technology. This technology would allow system developers to carefully choose the appropriate balance between offline verification of expressive properties (model checking) and online verification of important parts of the system's state space (runtime verification). We present several realistic examples where such technology appears necessary and a preliminary formalization of the idea.

Web applications rely heavily on client-side computation to examine and validate form inputs that are supplied by a user (e.g., credit card expiration date must be valid). This is typically done for two reasons: to reduce burden on the server and to avoid latencies in communicating with the server. However, when a server fails to replicate the validation performed on the client, it is potentially vulnerable to attack. In this paper, we present a novel approach for automatically detecting potential server-side vulnerabilities of this kind in existing (legacy) web applications through blackbox analysis. We discuss the design and implementation of NoTamper, a tool that realizes this approach. NoTamper has been employed to discover several previously unknown vulnerabilities in a number of open-source web applications and live web sites.

In feature-oriented software development, features distinguish different applications and a feature model abstractly represents the set of all possible applications for a given domain. Selecting a set of features that obey the feature model is the first step toward the synthesis of an application. In this paper, we present SmartForm, a web-based feature configuration tool that facilitates the process of feature selection. Its web-based feature selection user interface utilizes a web form generation tool Plato to perform real-time validation.

We present FML, a declarative policy language for managing the configuration of enterprise networks. FML was designed to replace the many disparate configuration mechanisms traditionally used to enforce policies within the enterprise. These include ACLs, VLANs, NATs, policy-routing, and proprietary admission control systems. FML balances the desires to express policies naturally and enforce policies efficiently. We have implemented FML and have used it to manage multiple operational enterprise networks for over a year.

Related: [hinrichs2008design]

Real-world automated reasoning systems must contend with inconsistencies and the vast amount of information stored in relational databases. In this paper, we introduce compilation techniques for inconsistency-tolerant reasoning over the combination of classical logic and a relational database. Our resolution-based algorithms address a quantifier-free, function-free fragment of first-order logic while leveraging off-the-shelf database technology for all data-intensive computation.

Related: [hinrichs2009inconsistency]

Collaborative Programming is characterized by groups of people issuing instructions to computer systems. Collaborative Programming languages differ from traditional programming languages because instruction sets can be incomplete and conflicting. An incomplete instruction set may only say what to do some of the time or what actions the system is forbidden from performing. A conflicting instruction set may simultaneously instruct the system to perform some action and forbid the system from performing that same action. Technology that supports Collaborative Programming must be able to combine independently authored instruction sets and be tolerant of incompleteness and conflicts. This paper introduces Collaborative Programming and through the discussion of two practical examples argues that tools from logic and automated reasoning form a good foundation for Collaborative Programming technology.

Computer scientists routinely design algorithms to efficiently solve problems found in nature. The resulting algorithms encapsulate the original problem as well as extra information about how to solve that problem; thus, nature's original description that says what the problem is has been augmented with information about how to solve it. In this paper, we investigate the automation of this process by concentrating on declarative languages, arguing that certain classes of declarative languages encode more information about how to solve a problem than others, and demonstrating techniques for automatically translating between two languages separated in the what-to-how spectrum.

Relational databases are one of the most industrially successful applications of logic in computer science, built for handling massive amounts of data. The power of the paradigm is clear both because of its widespread adoption and theoretical analysis. Today, automated theorem provers are not able to take advantage of database query engines and therefore do not routinely leverage that source of power. Extensional Reasoning is an approach to automated theorem proving where the machine automatically translates a logical entailment query into a database, a set of view definitions, and a database query such that the entailment query can be answered by answering the database query. This paper discusses the framework for Extensional Reasoning, describes algorithms that enable a theorem prover to leverage the power of the database in the case of axiomatically complete theories, and discusses theory resolution for handling incomplete theories.

Relational databases have had great industrial success in computer science. The power of the paradigm is made clear both by its widespread adoption and by theoretical analysis. Today, automated theorem provers are not able to take advantage of database query engines and therefore do not routinely leverage that source of power. Extensional Reasoning (ER) is an approach to automated theorem proving where the machine automatically translates a logical entailment query into a database, a set of view definitions, and a database query such that the entailment query can be answered by answering the database query. The techniques developed for ER to date are applicable only when the logical theory is axiomatically complete. This paper discusses techniques for reformulating an incomplete theory into a complete theory so that Extensional Reasoning techniques can be applied.

Logicians frequently use axiom schemata to encode (potentially infinite) sets of sentences with particular syntactic form. In this paper we examine a first-order language in which it is possible to write expressions that both describe sentences and assert the truth of the sentences so described. The effect of adding such expressions to a knowledge base is the same as directly including the set of described sentences.

In this paper, we describe an approach for automatically generating configurations for complex applications. Automated generation of system configurations is required to allow large-scale deployment of custom applications within utility computing environments. Our approach models the configuration management problem as an Object-Oriented Constraint Satisfaction Problem (OOCSP) that can be solved efficiently using a resolution-based theorem-prover. We outline the approach and discuss both the benefits of the approach as well as its limitations, and highlight certain unresolved issues that require further work. We demonstrate the viability of this approach using an e-Commerce site as an example, and provide results on the complexity and time required to solve for the configuration of such an application.

The FX-Agents project consisted of members of the Stanford Logic Group and industrial visitors from NEC and Intec Web and Genome working together to develop new technologies based upon the combination of Web services and techniques from artificial intelligence, using our experience in AI-based software agents. This two-year project ran from April 2001 until March 2002 and explored the then emerging functionality of Web services. This paper is a result of our findings. In particular, this paper discusses the shortcomings of current Web service standards like WSDL and how logical AI techniques like declarative commands, agents, and planning can be used to address some of these shortcomings. The primary problems that we address are automated Web service discovery and composition of Web services.

To date, most work regarding the formal analysis of access control schemes has focused on quantifying and comparing the expressive power of a set of schemes. Although expressive power is important, it is a property that exists in an absolute sense, detached from the application-specific context within which an access control scheme will ultimately be deployed. In this paper, we depart from the practice of absolute evaluation and introduce a mathematical framework aimed at assessing the suitability of existing access control schemes for a specific application. In our framework, an analyst first formally defines a workload representing the operational demands of the application and specifies metrics representing the pertinent costs. Reductions demonstrate how each candidate scheme---or some augmentation of it---can be used to safely implement the workload. Our framework assigns each such implementation a score based on the chosen cost metric and deems that the access control scheme with the highest scoring implementation is the one best suited for the application. We demonstrate our framework by presenting an example workload based on the requirements of a modern military, and exploring the suitability of a series of popular access control schemes for this workload.

Although the security community recommends that applications be designed for security from day one, today there is no formal technique for choosing the access control system that is best-suited for a particular application. In this paper, we present a formal framework and logic for comparing access control systems with respect to a particular application. The analyst's main task is to determine whether a given workload---a formalism that we develop to represent an application's access control demands---can be implemented correctly by each of several candidate access control systems. And because correctness by itself allows for implementations that few application developers would seriously consider, we develop several additional classifications for implementations that offer guarantees beyond correctness: homomorphic, non-interfering, safe, and succinct. The system that admits the implementation with the strongest guarantees is deemed the best fit for the application. We demonstrate the use of our framework by analyzing a workload that is anecdotally troublesome for the U.S. government's access control solution and present results for ten different access control models.

Logical policy-based access control models are greatly expressive and thus provide the flexibility for administrators to represent a wide variety of authorization policies. Extensional access control models, on the other hand, utilize simple data structures to better enable a less trained and non-administrative workforce to participate in the day-to-day operations of the system. In this paper, we formally study a hybrid approach, tag-based authorization (TBA), which combines the ease of use of extensional systems while still maintaining a meaningful degree of the expressiveness of logical systems. TBA employs an extensional data structure to represent metadata tags associated with subjects and objects, as well as a logical language for defining the access control policy in terms of those tags. We formally define TBA and introduce variants that include tag ontologies and delegation. We evaluate the resulting system by comparing to well-known extensional and logical access control models.

Modern web forms interact with the user in real-time by detecting errors and filling-in implied values, which in terms of automated reasoning amounts to SAT solving and theorem proving. This paper presents Plato, a compiler that automatically generates web forms that detect errors and fill-in implied values from declarative web form descriptions. Instead of writing HTML and JavaScript directly, web developers write an ontology in classical logic that describes the relationships between web form fields, and Plato automatically generates HTML to display the form and browser scripts to implement the requisite SAT solving and theorem proving. We discuss Plato's design and implementation and evaluate Plato's performance both analytically and empirically.

This paper presents the core algorithm for a tool implementing a declarative approach to web form development. Instead of writing Javascript to implement error detection and implied value computation, web developers write an ontology in classical logic that describes the relationships between web form fields, and the Javascript is generated automatically. To meet performance demands, the compilation of classical logic into Javascript uses relational databases as an intermediary; and, to address the well-known explosiveness problem of logical implication in the presence of contradictions (web form errors), our algorithm employs a paraconsistent form of logical implication.

Real-world automated reasoning systems must contend with inconsistencies and the vast amount of information stored in relational databases. In this paper, we introduce compilation techniques for inconsistency-tolerant reasoning over the combination of classical logic and a relational database. Our resolution-based algorithms address a quantifier-free, function-free fragment of first-order logic while leveraging off-the-shelf database technology for all data-intensive computation.

While traditional network security policies have been enforced by manual configuration of individual network components such as router ACLs, firewalls, NATs and VLANs, emerging enterprise network designs and products support global policies declared over high level abstractions. We further the evolution of simpler and more powerful network security mechanisms by designing, implementing, and testing a flow-based network security policy language and enforcement infrastructure. Our policy language, FSL, expresses basic network access controls, directionality in communication establishment (similar to NAT), network isolation (similar to VLANs), communication paths, and rate limits. FSL supports modular construction, distributed authorship, and efficient implementation. We have implemented FSL as the primary policy language for NOX, a network-wide control platform, and have deployed it within an operational network for over 10 months. We describe how supporting complex policy objectives and meeting the demanding performance requirements of network-wide policy enforcement have influenced the FSL language design and implementation.

Transfer Learning is a generalization of machine learning where instead of starting with no information when given the target task, the machine has already been able to learn in a source task. The degree to which the information gained by learning in the source is useful for the target is dependent on the relationship between source and target tasks. This paper proposes mathematical definitions for the relationships investigated in DARPA's Transfer Learning program.

Relational databases have had great industrial success in computer science; however, most automated theorem provers today do not take advantage of database query engines and therefore do not routinely leverage that source of power. Extensional Reasoning is an approach to automated deduction where the system automatically translates an entailment query expressed in classical logic into a query about a database system so that the answers to the two queries are the same. To prove the theorem, the system then evaluates the database query using an off-the-shelf database. <br><br>Extensional Reasoning was developed because many problems can be solved efficiently using a database but are naturally expressed using classical logic. In some cases, database query engines solve the database version of the query orders of magnitude faster than traditional theorem proving techniques solve the classical version. Extensional Reasoning helps us build systems that allow a non-expert to write problems down naturally, convert those problems to efficient representations automatically, and solve those problems using industrial-strength systems. <br><br>Conceptually, algorithms for performing Extensional Reasoning can be broken into two classes: those for complete theories and those for incomplete theories. A complete theory, one that can answer all the questions in its vocabulary, corresponds naturally to a relational database. Algorithms for this class of theories must recognize the theory is complete and then construct the appropriate database system. In the context of a logic with a finite domain, I present incomplete but low-order polynomial-time algorithms for performing these tasks. An incomplete theory, one for which there is some question in the vocabulary that cannot be answered, does not correspond naturally to a database system, and so the algorithms for performing Extensional Reasoning are more complex. In this case my approach is to construct a new, complete theory that captures the information pertinent to the original problem---a novel form of theory-completion. I present algorithms for performing this type of theory-completion in the same finite logic.

The specification for GDL, used in the yearly AAAI General Game Playing competition.

An object-oriented variant of the standard constraint satisfaction problem.

Herbrand logic has the same syntax as first-order logic but has Herbrand semantics. That is, the only models that exist in Herbrand logic are the Herbrand models. This logic is easier to learn than first-order logic and is often better suited for modeling and manipulating today's computer systems, the central concerns of computer science. In Herbrand logic, arithmetic using the natural numbers if finitely axiomatizable; however, neither entailment nor satisfiability are semi-decidable. Nevertheless, four of the most industrially successful applications of logic in computer science have been built within fragments of Herbrand logic: deductive databases, logic programming, constraint satisfaction, and formal verification. In this paper, we define Herbrand logic formally, prove several of its properties, discuss Goedel's incompleteness result with respect to Herbrand logic, and demonstrate how each of the four applications mentioned above can be formalized within Herbrand logic.

Unpublished technical note on proving that every player in every reachable state has at least one legal action in GDL games via constructing an abstract definition of the game.

Modern web Interfaces promote usability among end users by navigating them efficiently through a complex series of form inputs. However, the construction of these Web interfaces is poor from the point of view of developer friendliness and security. We propose the incorporation of behind-the-scences formal methods in web frameworks as an approach to achieve usability, efficiency and security of web interfaces, leading to their automatic, in-design certification.

Modern web forms interact with the user in real-time by detecting errors and filling-in implied values, which in terms of automated reasoning amounts to SAT solving and theorem proving. This paper presents Plato, a compiler that automatically generates web forms that detect errors and fill-in implied values from declarative web form descriptions. Instead of writing HTML and JavaScript directly, web developers write an ontology in classical logic that describes the relationships between web form fields, and Plato automatically generates HTML to display the form and browser scripts to implement the requisite SAT solving and theorem proving. We discuss Plato's design and implementation and evaluate its performance both analytically and empirically.

While traditional network security policies have been enforced by manual configuration of individual network components such as router ACLs, firewalls, NATs, and VLANs, emerging enterprise network designs and products support global policies declared over high level abstractions. We further the evolution of simpler and more powerful network security mechanisms by designing, implementing, and testing a flow-based network security policy language and enforcement infrastructure. Our policy language, FSL, expresses basic network access controls, directionality in communication establishment (similar to NAT), network isolation (similar to VLANs), communication paths, and rate limits. FSL supports modular construction, distributed authorship, and efficient implementation. We have implemented FSL as the primary policy language for NOX, a network-wide control platform, and have deployed it within an operational network for over 10 months. We describe how supporting complex policy objectives and meeting the demanding performance requirements of network-wide policy enforcement have influenced the FSL language design and implementation.

The prevalence of networked computer systems has enhanced a myriad of collaborative activities. Of special interest for computer science is the growing desire for large numbers of users to issue computer instructions in highly dynamic, loosely-coupled environments. In these settings, users might not communicate with each other outside of the instructions they issue, no user knows enough to write an the entire instruction set herself, and groups of users often disagree about the proper course of action.

We call such settings Collaborative Programming environments. Languages for these environments cope with issues not addressed in traditional approaches to programming. Because no user knows everything, instruction sets in Collaborative Programming languages can be incomplete, saying only what to do some of the time or forbidding certain actions. Because users sometimes disagree, instruction sets can be conflicting, simultaneously instructing the system to perform some action and forbidding the system from performing that same action. Technology that supports Collaborative Programming must be able to combine independently authored instruction sets and be tolerant of incompleteness and conflicts.

This talk introduces Collaborative Programming and through the discussion of two practical examples argues that tools from logic and automated reasoning form a good foundation for Collaborative Programming technology. At the same time, those examples provide challenges for researchers in logic and automated reasoning. The first example centers around a logical language for expressing network security policies; the second focuses on a generalization of traditional spreadsheets that allows users to impose relational constraints (as opposed to functional definitions) on cells in the spreadsheet. The talk concludes by discussing the tradeoffs for the example Collaborative Programming languages and techniques for leveraging those tradeoffs.

Much of the work done today on automated theorem proving focuses on developing and refining calculi that can handle every entailment query in the logic. Because of their generality, these uniform methods are often unable to take advantage of the special properties of the entailment query at hand. Nonuniform methods, on the other hand, do take advantage of special properties, which can result in performance improvements of several orders of magnitude over uniform methods; unfortunately, such techniques are not applicable to every query.

Extensional Reasoning (ER) is an approach to automated reasoning where the machine analyzes the entailment query at hand and determines whether or not to transform it into Datalog, i.e. a database, a set of views (implicit definitions for tables), and a database query. It is so named because one of the central concerns is determining which portion of the logical sentence set is to be converted into a database, i.e. which portion should be represented extensionally. This talk focuses on the transformation process: given an arbitrary entailment query, what algorithms can be used to automatically translate that query into Datalog? Unlike related work, extensional reasoning does not require certain symbols to have special properties but instead relies on model-theoretic and syntactic properties of the theory, e.g. axiomatic completeness. Extensional reasoning enables computer systems to solve important, well-understood problems using efficient, special-purpose techniques without losing the ability to solve all the problems expressible in the logic--it moves automated theorem provers toward the goal of practical generality.