Private Projects
Be Athletic Timer
Be Athletic Timer is a focused workout timer for interval training. Build any routine you need from activity types—work, rest, recovery, prepare, cooldown—and let the timer guide. Whether you're doing HIIT, Tabata, EMOM, or custom intervals, the app keeps you locked in with a clean, distraction-free timer.
Download on the App Store or visit the Be Athletic Timer Project Page.
PHP Webcore Framework
PHP Webcore Framework is a powerful, easy-to-use framework for building dynamic web applications.
The philosophy behind the framework is to provide an architecture and conceptual model for building web applications and to avoid recurring design problems by using object-based patterns and partitioning it into abstraction layers. The framework provides an object-oriented structure that specifies the relationships and interactions among classes and objects, enabling an easy-to-extend codebase. Its approach to software architecture focuses on providing flexibility, maintainability, and reusability.
Along with some powerful features, the PHP Webcore Framework provides a baseline for building web applications.
- Based on the Smarty template engine
- Role-based access control
- Module-based architecture
- Session and input control features
- Rapid application development
- Error handling and logging
PHP Webcore Lightweight Framework
PHP Lightweight Framework is the lightweight edition of the PHP Webcore Framework.
Major Research Projects
TreatJS: Higher-Order Contracts for JavaScript
TreatJS is a language-embedded, higher-order contract system for JavaScript that enforces contracts through run-time monitoring. Beyond providing the standard abstractions for building higher-order contracts (base, function, and object contracts), TreatJS's novel contributions include a guarantee of non-interfering contract execution, a systematic approach to blame assignment, support for contracts in the style of union and intersection types, and a 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 JavaScript library, and all aspects of a contract can be specified using the full JavaScript language.
See the Project Website of TreatJS
DecentJS
DecentJS is a language-embedded sandbox for JavaScript. It enables scripts to run with a configurable degree of isolation and fine-grained access control. It provides a transactional scope in which effects are logged for review by the access control policy. After inspecting the log, effects can be committed to the application state or rolled back.
The implementation relies on JavaScript proxies to guarantee full interposition across the entire language and for all code, including dynamically loaded scripts and code injected via eval.
Transparent Object Proxies for JavaScript
A proxy, or wrapper, is an object that mediates access to an arbitrary target object. Proxies are widely used for resource management, accessing remote objects, enforcing access control, limiting an object's functionality, or enhancing an object's interface. Ideally, a proxy is indistinguishable from other objects, so running a program with an interposed proxy should yield 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, each distinct from the target, a single target object may acquire multiple identities---it suffers from schizophrenia! Even worse, there is no single cure for this schizophrenia because the desired behavior depends on the use case.
Unfortunately, current proxy implementations are tied to specific use cases, making it difficult to adapt them to other requirements. We examine the issue of transparency in detail, consider various proxy use cases, discuss approaches to achieving transparency, and propose two designs that cannot be bypassed by the programmer but that require modest modifications to 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 using path specifications that resemble regular expressions. To overcome the limitations of the JSConTest implementation, we redesigned and reimplemented effect monitoring by taking advantage 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, which extend basic regular expressions with intersection and complement operators and consider regular expressions over potentially infinite character sets. The algorithm avoids translating to an expression-equivalent automaton and provides a purely symbolic term rewriting system for solving regular expression inequalities.
We present a new symbolic decision procedure for the containment problem, based on Brzozowski's regular expression derivatives and Antimirov's rewriting approach for checking containment. We generalize Brzozowski's syntactic derivative operator to two derivative operators that operate 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 provides a viable basis for investigating data integrity, ensuring confidentiality, and 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 tainting semantics. We prove the correctness of the tainting semantics, the soundness of the abstraction, a noninterference property, and the termination of the analysis.