Results

Results and Resources

Over the course of our work we will keep making code and other resources publicly available.

• The JSExplain Report is available here.
• Final Report
  The final report of the project is available here.
• JSCert (CELTIQUE)We have made some of our presentations available to describe the formal model. Please contact the CELTIQUE team (Martin Bodin, ‎Alan Schmitt, ‎Thomas Jensen and Frédéric Besson) if you have any queries related to these semantics.Presentations
  • Toward a Certified Information Flows Analysis for JavaScript
  • Pretty-big-step-semantics-based Certified Abstract Interpretation
  • Toward a Certified Information Flows Analysis for JavaScript

  The JSCert project maintains its repository on GitHub and is publicly available. The project can be accessed at https://github.com/jscert/jscert for instructions on downloading as well as on the required dependencies. It is maintained under the git version control system and can be downloaded by executing the following command on your terminal.

  git clone https://github.com/jscert/jscert.git

   

  DISCLAIMER: CELTIQUE and SecCloud do not take any responsibility for any damage that could be caused through running this application. Run at own risk.

• Lamfa (ASCOLA)

  We built several prototypes of instrumented lambda-calculus interpreters with information flow analyses, in order to identify and classify the language mechanisms needed for instrumentation. The prototypes, and research notes, are available on the following git repository hosted on GitHub: https://github.com/fmdkdd/lamfa. Any queries regarding this can be directed to the ASCOLA team (Florent Marchand de Kerchove, Jacques Noyé, Mario Südholt). It can be cloned using the command.

  git clone https://github.com/fmdkdd/lamfa.git

  A snapshot of the recent results are also conveyed in the following presentation.

  Presentation

  • Modular Instrumentation of Dynamic Program Analyses
• InFlow (CIDRE)We have made our presentation describing the current work available below. Any queries regarding this can be directed to the CIDRE team comprising of Deepak Subramanian, Guillaume Hiet, Christophe Bidan and Ludovic Mé.Presentation
  • Preventive information flow control through a mechanism of split addresses

  We have designed a vulnerable server for testing the security mechanisms of our model. A vulnerable server implies that the application running on the server is known to have exploitable vulnerabilities. This server is provided by the CIDRE team to analyze some well-known vulnerabilities and to envision effective models in reducing their impact. Consequently we restrict access to this server to team members and partners. Please contact the CIDRE team for information about direct access to this server. The code is freely distributed to be run at your own risk. It requires a Java 7 application server with web profile to run.

  This project’s repository is can be accessed through git (version control system). Please run the following command through your terminal to obtain a copy of this repository.

  git clone https://gforge.inria.fr/git/inflow/inflow.git

   

  Over the course of our work, we have modified Zaphod Facets to correct some of the bugs and features to ensure a fair comparison with our approach. We maintain this modified version at a public repository and this version can be downloaded using the following command.

  git clone https://bitbucket.org/subudeepak/zaphod-facets.git