Joseph P. Near

Postdoctoral Researcher
University of California, Berkeley
Office: 725 Soda Hall
E-mail: jnear at berkeley dot edu

[ CV | Research statement | Teaching statement ]

[ Projects | Publications | Press | Teaching ]


Research

My research interests include data privacy, security, programming languages, and software engineering. My research to date focuses on the theory, design, and implementation of algorithms and programming systems (programming languages, static analyses, and runtime systems) that enable provable security and privacy.


Projects

FLEX and Elastic Sensitivity: Differential Privacy for SQL Queries

FLEX is a system for enforcing differential privacy for SQL queries that works with a standard SQL database. Elastic sensitivity represents the theory behind FLEX: it is the first tractable approach to leverage local sensitivity for queries with general equijoins. The key insight of our approach is to model the impact of each join in the query using precomputed metrics about the frequency of join keys in the true database. FLEX and elastic sensitivity are compatible with standard, unmodified SQL databases, support queries expressed in standard SQL, and integrate easily into existing data environments.

Space

Space is a nearly automatic tool for finding access control bugs in web applications. Space uses symbolic execution to generate verification conditions, and checks them against a library of formal access control patterns using a bounded verifier. Space has been used to uncover 23 previously unknown security bugs in 50 open source Rails applications.

Derailer

Derailer is a visualization-guided static analysis for finding security bugs in web applications. Derailer uses an automatic static analysis to produce a visual representation of the information flows within a Ruby on Rails application. The visualization organizes the results of the analysis in a tree, and allows filtering out allowed information flows to find ones representing security bugs.

Rubicon

Rubicon is a lightweight bounded verifier for web applications. It automatically checks verification conditions against a specification written by the developer using the Alloy Analyzer. Rubicon generates verification conditions using symbolic execution of a Ruby on Rails application. Rubicon leverages the standard Ruby interpreter to perform symbolic execution, ensuring compatibility with Rails and reducing complexity (the library is just 1000 lines of code). Rubicon scales to real open source applications, with analyses typically taking fewer than 10 seconds.


Publications

  • Towards practical differential privacy for SQL queries.
    Noah Johnson, Joseph P. Near, and Dawn Song.
    Conditionally accepted in Proceedings of the 34th International Conference on Very Large Data Bases, 2018.

  • Towards practical differential privacy for SQL queries.
    Noah Johnson, Joseph P. Near, and Dawn Song.
    CoRR, abs/1706.09479, 2017

  • Finding security bugs in web applications using a catalog of access control patterns.
    Joseph P. Near and Daniel Jackson.
    In Proceedings of the 38th ACM/IEEE International Conference on Software Engineering (ICSE), 2016.

  • Alloy*: A general-purpose higher-order relational constraint solver.
    Aleksandar Milicevic, Joseph P. Near, Eunsuk Kang, and Daniel Jackson.
    In Proceedings of the 37th ACM/IEEE International Ionference on Software Engineering (ICSE), 2015.
    Distinguished paper award.

  • Finding Security Bugs in Web Applications using Domain-Specific Static Analysis.
    Joseph P. Near.
    MIT PhD Thesis, 2015.

  • Derailer: Interactive Security Analysis for Web Applications.
    Joseph P. Near and Daniel Jackson.
    In Proceedings of the 29th IEEE/ACM International Conference on Automated Software Engineering (ASE), 2014. (pdf)

  • Alloy*: A higher-order relational constraint solver.
    Aleksandar Milicevic, Joseph P. Near, Eunsuk Kang, and Daniel Jackson.
    Technical Report MIT-CSAIL-TR-2014-018, Computer Science and Artificial Intelligence Lab, Massachusetts Institute of Technology, Cambridge, Massachusetts, 2014. (link)

  • Symbolic execution for (almost) free: Hijacking an existing implementation to perform symbolic execution.
    Joseph P. Near and Daniel Jackson.
    Technical Report MIT-CSAIL-TR-2014-007, Computer Science and Artificial Intelligence Lab, Massachusetts Institute of Technology, Cambridge, Massachusetts, April 2014. (pdf)

  • Applications and extensions of Alloy: past, present and future.
    Emina Torlak, Mana Taghdiri, Greg Dennis, and Joseph P. Near.
    In Mathematical Structures in Computer Science, volume 23 number 4, 2013.

  • Rubicon: bounded verification of web applications.
    Joseph P. Near and Daniel Jackson.
    In Proceedings of the 20th International Symposium on the Foundations of Software Engineering (FSE), 2012. (pdf)

  • A lightweight code analysis and its role in evaluation of a dependability case.
    Joseph P. Near, Aleksandar Milicevic, Eunsuk Kang and Daniel Jackson.
    In Proceedings of the 33rd International Conference on Software Engineering (ICSE), 2011.

  • An Imperative Extension to Alloy and a Compiler for its Execution.
    Joseph P. Near.
    MIT Masters Thesis, 2010. (pdf)

  • From Relational Specifications to Logic Programs.
    Joseph P. Near.
    In Proceedings of the 26th International Conference on Logic Programming (Technical Communications), 2010. (pdf)

  • An Imperative Extension to Alloy.
    Joseph P. Near and Daniel Jackson.
    In Proceedings of the 2nd International Conference on Abstract State Machines, Alloy, B and Z, 2010. (pdf)

  • Equality and Hashing for (almost) Free: Generating Implementations from Abstraction Functions.
    Derek Rayside, Zev Benjamin, Rishabh Singh, Joseph P. Near, Aleksandar Milicevic, and Daniel Jackson.
    In Proceedings of the 31st International Conference on Software Engineering, 2009.

  • alphaleanTAP: A Declarative Theorem Prover for First-Order Classical Logic.
    Joseph P. Near, William E. Byrd, and Daniel P. Friedman.
    In Proceedings of the 24th International Conference on Logic Programming, 2008. (pdf)

Selected Press


Teaching


725 Soda Hall Berkeley, CA 94720-1776