(T3) Programación de Seguridad mediante Bibliotecas: Teoría y Práctica con Haskell y Python

cabezal
  • Profesor:  Alejandro Russo (Chalmers University of Technology, Suecia)
  • Horario: Lunes a viernes de 13:30 a 16:30 horas
  • Aula: A definir (Pabellón 1)
  • Idioma: Castellano 
  • Evaluación: Trabajo Práctico de tipo take-home

Resumen breve: A lo largo de los años se han desarrollado varios lenguajes especialmente diseñados para garantizar la confidencialidad o la integridad de la información. El problema de estos lenguajes es que no tuvieron un impacto demasiado amplio en el proceso de desarrollo de software. Por otro lado, se ha demostrado que es posible garantizar un conjunto de políticas de seguridad simplemente usando bibliotecas sobre lenguajes ya conocidos. Este enfoque tiene la ventaja de motivar una adopción más rápida y menos problemática por parte de los programadores. El objetivo del curso es describir los principios detrás de las librerías que proveen seguridad en el flujo de la información (IFS). El curso va a centrarnos en Haskell y en cómo las monadas pueden garantizarnos que las políticas de seguridad son cumplidas, esto es, lograr que nuestros secretos no sean revelados o que inputs no confiables produzcan inseguridades en el sistema. También mostraremos cómo en Python pueden usarse despachos dinámicos y decoradores para implementar una biblioteca que nos provea la capacidad de realizar "taint-analysis", una forma especial de IFS. El único prerequisito para los estudiantes son nociones básicas de programación funcional.

Programa tentativo: 
Día 1: Principales funciones en Haskell y mónadas. Día 2: Mónadas para seguridad. Día 3: Correctitud de las mónadas Sec e IO. Día 4: Políticas de integridad. Día 5: Otras para seguridad.

Programa extendido y actualizado (ver fuente original):

Day 1 and 2

Complementary reading

  • Monads: A very known paper: Monads for functional programming, Philip Wadler, In Advanced Functional Programming, First International Spring School on Advanced Functional Programming Techniques-Tutorial Text, pages 24–52, London, UK, 1995. Springer-Verlag. If the paper is difficult to follow, you migth want to check the whole Chapter 18 from Haskell: The Craft of Functional Programming (see above).
  • Language-based security : Language-Based Security, Dexter Kozen, In Mathematical Foundations of Computer Science, 1999. (easy reading)
  • Information-flow security : Language-Based Information-Flow Security, Andrei Sabelfeld and Andrew C. Myers, IEEE Journal on Selected Areas in Communications, 2003. (a very well-known survey)
  • Declassification : Declassification: Dimensions and principles, Andrei Sabelfeld and David Sands, In Proceedings of the 18th IEEE Workshop on Computer Security Foundations, 2005. (a nice survey of the area)

Day 3

Complementary reading

Day 4

Complementary reading

Day 5

  • Secure Multi-Execution in Haskell , Mauro Jaskelioff and Alejandro Russo. In Proceedings of Andrei Ershov International Conference on Perspectives of System Informatics (PSI'11), Akademgorodok, Novosibirsk, Russia, June 27-July 1, 2011. LNCS, Springer-Verlag.

Complementary reading

 

 

  • Bibliografía recomendada: 

• K. J. Biba. Integrity considerations for secure computer systems. Technical Report ESD-TR-76-372, USAF Electronic Systems Division, Bedford, MA, April 1977.
• S. Chong and A. C. Myers. Language-based information erasure. In Proc. IEEE Computer Security Foundations Workshop (CSFW), pages 241–254, June 2005.
• J.J. Conti and A. Russo. A taint mode for Phyton via a library. In Proc. NordSec workshops, Helsinki, Finland, 2010. Springer-Verlag.
• D. E. Denning and P. J. Denning. Certification of programs for secure information flow. Comm. of the ACM, 20(7): 504–513, July 1977.
• A. Disertholf. Master thesis: Providing integrity policies as a library in Haskell. chalmers university of technology.
Available at http://www.cse.chalmers.se/~russo/albert.htm, 2010.
• J. A. Goguen and J. Meseguer. Security policies and security models. In Proc. IEEE Symp. on Security and Privacy, pages 11–20, April 1982.
• S. Hunt and D. Sands. Just forget it – the semantics and enforcement of information erasure. In Proc. of the European Symposium on Programming, LNCS. Springer Verlag, 2008.
• P. Li, Y. Mao, and S. Zdancewic. Information integrity policies. In Proc. of the workshop on formal aspects in Security & Trust (FAST, 2003.
• A. C. Myers, A. Sabelfeld, and S. Zdancewic. Enforcing robust declassification. In Proc. IEEE Computer Security Foundations Workshop (CSFW), pages 172–186, June 2004.
• Phu H. Phung, David Sands, and Andrey Chudnov. Lightweight self-protecting javascript. In R. Safavi-Naini and V. Varadharajan, editors, ACM Symposium on Information, Computer and Communications Security (ASIACCS 2009), Sydney, Australia, March 2009. ACM Press.
• A. Russo, K. Claessen, and J. Hughes. A library for light-weight information-flow security in Haskell. In Proc. ACM SIGPLAN Symposium on Haskell (HASKELL), pages 13–24. ACM Press, September 2008.
• F. Del Tedesco, A. Russo, and D. Sands. Implementing erasure policies using taint analysis. In Proc. NordSec workshops, Helsinki, Finland, 2010. Springer-Verlag.
• Simon Thompson. The Haskell: The Craft of Functional Programming. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 2nd edition, 1999. ISBN 0201342758.
• Philip Wadler. Monads for functional programming. In Advanced Functional Programming, First International Spring School on Advanced Functional Programming Techniques-Tutorial Text, pages 24–52, London, UK, 1995. Springer-Verlag.

Notas Finales

pie