IST Project -- Hardened Golo : Giving some confidence into your Golo code
- Nicolas Stouls (firstname.lastname@example.org)
- Oscar Carrillo (email@example.com)
Number of students
1 or 2.
Golo is a simple, dynamic, weakly-typed language for the JVM created in 2012 as part of the research
activities of the DynaMid group of the Centre of Innovation in Telecommunications and Integration
of service aka CITI Laboratory.
This language adds the dynamicity into the objects. It means that objects themselves
can evolve during time, by adding new methods, new attributs, ...
It's also possible to dynamically modify classes provided by the standard API. By instance by adding new method into String. Its called the augmentation.
HardenedGolo is a project aiming in statically verify some Golo code. The static verification could be only the verification of the
language semantic (a division is not made by 0) or the verification of the respect of a specification. We are then currently adding
the possibility to describe a specification into a Golo program in a JML-like manner, with the syntax of WhyML.
This IST project is in the context of this new feature.
In this project, many aspects could be developped, according to the preferences of the students, among them:
- Test and complete parser for First Order Logic specification, with the associate intermediate representation
- Integration into Gradle whith non-regression tests
- Add type information into intermediate representation (IR)
- Add type propagation / induction into IR
- Extend the JGolo specification language with some new primitives expressing that a method/an attribute exists or does not exist into an object.
- Considere specific WhyML functions into JGolo specification (i.e. to_int, of_int, ...)
- Propose a new name for the specification language (or found an explanation for "Why JGolo ?")
 Golo : http://golo-lang.org/
 Krakatoa : http://krakatoa.lri.fr/
 De Win, B., Vanhaute, B., & De Decker, B. (2002). Security through aspect-oriented programming. In Advances in Network and Distributed Systems Security (pp. 125-138). Springer US.
 Guitton, J., Kanig, J., & Moy, Y. (2011). Why hi-lite ada. Rustan, et al., 27-39, Boogie - 1st international workshop on Intermediate Verification Languages.
 Goichon, F., Salagnac, G., Parrend, P., & Frénot, S. (2013). Static vulnerability detection in Java service-oriented components. Journal of Computer Virology and Hacking Techniques, 9(1), 15-26.
 Laurent, R. (2016). Hardened Golo : Donnez de la confiance en votre code Golo, https://hal.inria.fr/hal-01354836/