Major Research Projects
TreatJS: Higher-Order Contracts for JavaScript
TreatJS is a language embedded, higher-order contract system for JavaScript which enforces contracts by run-time monitoring. Beyond providing the standard abstractions for building higher-order contracts (base, function, and object contracts), TreatJS's novel contributions are its guarantee of a non-interfering contract execution, its systematic approach to blame assignment, its support for contracts in the style of union and intersection types, and its notion of a parameterized contract scope, which is the building block for composable run-time generated contracts that generalize dependent function contracts.
TreatJS is implemented as a library in JavaScrip and all aspects of a contract can be specified using the full JavaScript language.
See the Project Website of TreatJS or try it online!
DecentJS
DecentJS is a language-embedded sandbox for JavaScript. It enables scripts to run in a configurable degree of isolation with fine-grained access control. It provides a transactional scope in which effects are logged for review by the access control policy. After inspection of the log, effects can be committed to the application state or rolled back.
The implementation relies on JavaScript proxies to guarantee full interposition for the full language and for all code, including dynamically loaded scripts and code injected via eval.
Transparent Obejct Proxies for JavaScript
A proxy, or wrapper, is an object that mediates access to an arbitrary target object. Proxies are widely used to perform resource management, access remote objects, impose access control, restrict the functionality of an object, or to enhance the interface of an object. Ideally, a proxy is not distinguishable from other objects so that running a program with an interposed proxy should lead to the same outcome as running the program with the target object, unless the proxy imposes restrictions.
Proxies introduce a subtle problem. Because a target object may have any number of proxy objects, which are all different from the target, a single target object may obtain multiple identities---it suffers from schizophrenia! Even worse, it turns out that there is no single cure for this schizophrenia because the desired behavior depends on the use case.
Unfortunately, current proxy implementations are committed to particular use cases, which makes it hard to adapt them to uses with different requirements. We examine the issue with transparency in detail, consider various use cases for proxies, discuss different approaches to obtain transparency, and propose two designs that cannot be bypassed by the programmer but that require modest modifications in the JavaScript engine.
JSConTest2: Efficient Access Analysis Using JavaScript Proxies
JSConTest introduced the notions of effect monitoring and dynamic effect inference for JavaScript. It enables the description of effects with path specifications resembling regular expressions. To overcome the limitations of the JSConTest implementation, we redesigned and reimplemented effect monitoring by taking advantange of JavaScript proxies. Our new design guarantees full interposition; it is not restricted to a subset of JavaScript; it is self-maintaining; and its scalability to large programs is significantly better than with JSConTest.
See the Project Website of JSConTest2.
Efficient Solving of Regular Expression Inequalities
This work presents a new solution to the containment problem for extended regular expressions that extends basic regular expressions with intersection and complement operators and consider regular expressions on infinite alphabets based on potentially infinite character sets. The algorithm avoids the translation to an expression-equivalent automaton and provides a purely symbolic term rewriting systems for solving regular expressions inequalities.
We give a new symbolic decision procedure for the containment problem based on Brzozowski's regular expression derivatives and Antimirov's rewriting approach to check containment. We generalize Brzozowski's syntactic derivative operator to two derivative operators that work with respect to (potentially infinite) representable character sets.
Type-based Dependency Analysis
Dependency analysis is a program analysis that determines potential data flow between program points. While it is not a security analysis per se, it is a viable basis for investigating data integrity, for ensuring confidentiality, and for guaranteeing sanitization. A noninterference property can be stated and proved for the dependency analysis.
We have designed and implemented a dependency analysis for JavaScript. We formalize this analysis as an abstraction of a tainting semantics. We prove the correctness of the tainting semantics, the soundness of the abstraction, a noninterference property, and the termination of the analysis.
See the Project Website of TbDA.
Private Projects
PHP Webcore Framework
PHP PHP Webcore Framework is a powerful and easy-to-use PHP framework designed to build dynamic web applications.
The philosophy behind the framework is towards giving an architecture and conceptual model to build web-application and to avoid recurring design-problems by using object-based patterns and partitioning it into abstraction layers.
The framework gives an object-oriented structure specifinging the relationships and interactions between classes and objects, building an easy-exdenable structuring of code. Its approach to software architecture is about providing flexibility, maintainability and reusibility.
Along with some powerful features the PHP Webcode Framework builds a baseline for building web-application.
- Based an the Smarty template engine
- Based on the PHP Database Interface
- Role-based access control
- Module-based architecture
- Session and input control features
- Rapid application development
- Error handling and logging
PHP Webcore Lightweight Framework
The PHP Lightweight Framework is the lightweight edition of the PHP Webcore Framework.
