Future

Current goals

  • Polish the code so that it can be released.
  • Computation of output effects is still not fully correct: there are some features of Java (most notably exceptions, but also class initialization blocks) which make effects hard to compute, and may also cause a great loss of precision.
  • Various parts of the website need work.
  • The context abstraction as well as the policy (syntactic monoid) can already easily be changed; a future option would be to specify them in an 'options' file for the analyzer.
  • Clean specification of type of "output" method.

 

Long-term goals

practice

  • test analyzer on real code, model actual security policy
  • check expressivity/speed/helpfulness for programmer
  • improve tool usability

theory 

  • full type system for FJEUS
  • soundness proof
  • refined object types (classes with region annotations)
  • connection of the implemented type system for Java to the FJEUS type system (formal or informal)
  • find generalisations or limits of entire approach