eXactas.org - Eventos

Symposium on Automatic Program Verification (14/02/2009 - 15/02/2009)

Fecha: 14/02/2009

APV 2009
Automatic Program Verification
http://se.ethz.ch/apv/
February 14-15, 2009
Rio IV, Argentina
--------------------------------------------------------------------

Automatic software verification is once again at the forefront of research in computer science, thanks to a combination of novel techniques and more powerful hardware to implement them. The aim of the ASV symposium is to bring together researchers to exchange and develop new ideas in all aspects of software verification, from design to implementation.

Topics of interest include but are not limited to:

* automatic theorem provers
* static program analysis
* model checking
* tool descriptions and experience reports
* case studies

Festival Latinoamericano de Instalaci�n de Software Libre (26/04/2008)

Fecha: 26/04/2008

�Qu� es el FLISoL?

El Festival Latinoamericano de Instalaci�n de Software Libre (FLISoL) es el evento de difusi�n de Software Libre m�s grande en Latinoam�rica. Se realiza desde el a�o 2005 y su principal objetivo es promover el uso del software libre, dando a conocer al p�blico en general su filosof�a, alcances, avances y desarrollo.

Para tal fin, las diversas comunidades locales de software libre (en cada pa�s, en cada ciudad/localidad), organizan simult�neamente eventos en los que se instala, de manera gratuita y totalmente legal, software libre en las computadoras que llevan los asistentes. Adem�s, en forma paralela, se ofrecen charlas, ponencias y talleres, sobre tem�ticas locales, nacionales y latinoamericanas en torno al Software Libre, en toda su gama de expresiones: art�stica, acad�mica, empresarial y social.

El FLISOL 2008 se llevar� a cabo el s�bado 26 de abril.

�Qui�n organiza el FLISoL?

La Comunidad de Software Libre en Latinoam�rica, conformada por personas y grupos de diversa �ndole, con el apoyo de otras entidades, principalmente educativas, y algunos patrocinadores de los eventos en cada localidad.

�A qui�n est� dirigido el evento?

El evento est� dirigido a todo tipo de p�blico: estudiantes, acad�micos, empresarios, trabajadores, funcionarios p�blicos, entusiastas y aun personas que no poseen mucho conocimiento inform�tico. Si posees o no conocimientos e intereses en inform�tica, licencias, derecho de autor/copyright y dem�s �reas de la ciencia y la tecnolog�a, d�jate tentar, asiste y participa del evento. Nuestro objetivo es compartir conocimientos y ansias de libertad.

�Cu�nto cuesta la asistencia al evento?

La asistencia al evento es totalmente libre y gratuita.

�Qu� beneficios obtengo asistiendo al FLISoL?

�Y qu� pierdes?... Entre algunos beneficios, tendr�s la oportunidad de instalar software libre en tu computadora, apreciar qu� es una real y segura alternativa a otros modelos de desarrollo y distribuci�n de software, informarte sobre la filosof�a, cultura y organizaci�n alrededor del mismo, y conocer las experiencias, desarrollos e investigaciones de grupos y entidades en torno al Software Libre, tanto a nivel local, nacional e internacional.

Tal vez encuentres una alternativa/soluci�n en software libre para ti, tu empresa, colegio, universidad e, incluso, para tu gobierno. Podr�s aclarar tus dudas acerca de los temas relacionados y, quiz�s encuentres en el software libre, una alternativa de investigaci�n, empleo y desarrollo tecnol�gico.

�C�mo puedo saber si en mi ciudad se realizar� el evento?

Sigue este enlace. Podr�s encontrar mayor informaci�n, el lugar de realizaci�n del evento y los contactos respectivos de las personas, grupos y entidades a cargo. Si por otra parte, en tu pa�s y/o ciudad no hay programado evento todav�a y eres un entusiasta o est�s interesado en organizar y/o promover un evento, por favor consulta esta informaci�n.

Festival Latinoamericano de Instalaci�n de Software Libre (26/04/2008)

Fecha: 26/04/2008

�Qu� es el FLISoL?

�Qui�n organiza el FLISoL?

�A qui�n est� dirigido el evento?

�Cu�nto cuesta la asistencia al evento?

La asistencia al evento es totalmente libre y gratuita.

�Qu� beneficios obtengo asistiendo al FLISoL?

�C�mo puedo saber si en mi ciudad se realizar� el evento?

Presentaci�n de Tesina de Pablo Mata (21/12/2007)

Fecha: 21/12/2007

Presentaci�n de Tesina

T�tulo:
"Flowx: Implementaci�n de No Interferencia en Linux"

Tesista:
Pablo Mata

D�a:
Viernes 21 de Diciembre

Hora:
12:00hs

Lugar:
Aula 23, FCEIA (Pellegrini 250)

abstract:

Esta tesina describe los pasos para la creaci�n de un m�dulo de seguridad para un sistema operativo Linux, el cual busca imponer no interferencia y control del flujo de la informaci�n seg�n un modelo formal desarrollado por M. Cristi�. El objetivo es proteger al sistema tanto de caballos de Troya como de ciertas clases de canales encubiertos que los mecanismos de control de acceso tradicionales no pueden evitar.
El m�dulo se implement� sobre el framework de seguridad que introduce Linux en sus kernels 2.6, llamado Linux Security Modules (LSM), el cual provee diferentes hooks en distintos puntos cr�ticos del kernel, con la intenci�n de que un m�dulo implemente chequeos, comprobaciones o diferentes tareas a la hora de que cada hook sea invocado.
Como resultado se busca desarrollar un prototipo de seguridad que adem�s de asegurar la confidencialidad de la informaci�n del sistema, no penalice de manera significativa la performance de �ste y sea 100% compatible con el software existente.

Presentaci�n de Tesina de Alejandro D�az-Caro (Janus) (21/12/2007)

Fecha: 21/12/2007

Presentaci�n de Tesina

T�tulo:
"Agregando medici�n al C�lculo de van Tonder"

Tesista:
Alejandro D�az-Caro

D�a:
Viernes 21 de Diciembre

Hora:
10:45hs

Lugar:
Aula 23, FCEIA (Pellegrini 250)

abstract:

El �rea de los lenguajes de programaci�n cu�nticos se est� desarrollando a una gran velocidad. En particular, se han definido varias extensiones al Lambda C�lculo que proveen la sintaxis y sem�ntica necesarias para modelar algoritmos cu�nticos.
Uno de los trabajos m�s influyentes en este sentido es el \lambda_q de Andr� van Tonder[1]. Este es un Lambda C�lculo, definido mediante su sem�ntica operacional, para c�mputos puramente cu�nticos: la medici�n no es parte del c�lculo.
La intenci�n de este trabajo es agregar medici�n al \lambda_q, para lo cual nos valemos de algunas herramientas del Lambda C�lculo probabil�stico definido por Di Pierro, Hanking y Wiklicky en [2]. Adem�s, siguiendo la l�nea de trabajo de van Tonder, tambi�n hacemos uso de la la sintaxis para la l�gica lineal de Philip Wadler[3].

Ref:
[1] A. van Tonder, "A Lambda Calculus for Quantum Computation", SIAM J. Comput. 33(5), Society for Industrial and Applied Mathematics, 1109�1135, 2004
[2] A. Di Pierro, C. Hankin y H. Wiklicky, "Probabilistic Lambda-calculus and Quantitative Program Analysis", Journal of Logic and Computation 15(2), 159�179, 2005
[3] P. Wadler, "A Syntax for Linear Logic", Proceedings of the 9th International Conference on Mathematical Foundations of Programming Semantics, Springer-Verlag, 513�529, 1994

Charla "Controlling timing channels in multithreaded programs" (20/12/2007 - 06/12/2007)

Fecha: 20/12/2007

Charla : Controlling timing channels in multithreaded programs

Disertante: Alejandro Russo

Fecha y Lugar : 20 de Diciembre 2007, Aula 23, 15.00hs, FCEIA.

Duraci�n: 45 minutos

Conocimiento previo recomendable:
- Haber programado en alg�n lenguaje imperativo como Pascal o C
- Haber programado en alg�n lenguaje concurrente

Resumen
-------------

Controlar el flujo de informaci�n (information flow) en programas
multithreaded es todav�a un problema abierto. En particular, el controlar
que no haya flujo de informaci�n desde datos secretos a datos p�blicos, lo
cual es conocido como no interferencia. Programas concurrentes introducen
canales encubiertos (covert channels) por donde informaci�n puede
ser transmitida inadvertidamente. En particular, uno de los
canales encubiertos que dificultan el control del flujo de informaci�n
es llamado 'canal encubierto de tiempo interno' (internal timing covert
channel). Informaci�n es transmitida por este canal cuando informaci�n
secreta afecta el tiempo de ejecuci�n de un thread, que mediante el
scheduler, afecta el orden en que algunos eventos p�blicos
son realizados. Volpano y Smith propusieron una primitiva especial llamada
protect. Por definici�n, protect(c) ejecuta c at�micamente realizando un paso
en la sem�ntica del programa. El canal encubierto de tiempo interno puede ser
eliminado si todo computo que toma alguna decisi�n basada en datos secretos
es ejecutado dentro de este comando. Sin embargo, implementar protect no es
algo trivial.

Esta tesis introduce una novedosa interacci�n entre threads y el scheduler
para solucionar el problema de canales encubiertos de tiempo interno. Como
resultado de esa interacci�n, se obtiene una permisiva especificaci�n de no
interferencia y un sistema de tipos composicional. El sistema de tipos
garantiza no interferencia para una amplia clase de schedulers y
permite creaci�n de threads en tiempo de ejecuci�n (runtime).

En algunas situaciones, la modificaci�n del entorno de ejecuci�n (runtime
environment) puede ser un requerimiento no viable. Para tales escenarios,
esta tesis tambi�n presenta dos transformaciones de programas que eliminan
la necesidad de tener la primitiva especial protect o alguna interacci�n
especial con el scheduler. La primera transformaci�n de programas contempla
c�digo que es ejecutado bajo schedulers cooperativos. B�sicamente, la
transformaci�n garantiza que las threads no cedan el control cuando est�n
dentro de un comando que toma decisiones basadas en informaci�n
secreta. La segunda transformaci�n de c�digo elimina el canal encubierto de
tiempo interno cuando el scheduler es preemtivo y se comporta como
round-robin. La transformaci�n introduce, y cuidadosamente sincroniza, la
creaci�n de nuevos threads que se dedican a realizar c�mputos que dependen
de datos secretos.

Como una evaluaci�n de algunas de las ideas descriptas anteriormente, esta
tesis tambi�n presenta una implementaci�n en Haskell de una librer�a que
provee control del flujo de informaci�n para programas multithread. La
implementaci�n incluye un caso de estudio de online-shopping. El caso de
estudio revelo que el canal encubierto de tiempo interno es f�cil de
aprovechar para revelar informaci�n secreta, como n�meros de tarjetas de
cr�dito, en un tiempo razonable. Adem�s, mostramos como la librer�a
ayuda a eliminar este canal encubierto en el caso de estudio. Hasta la fecha
de publicaci�n, esta en la primera herramienta que permite controlar el flujo
de informaci�n en programas concurrentes y la primera implementaci�n de una
caso de estudio que involucra concurrencia y flujo de informaci�n.

Intro al Entorno de Aprendizaje Colaborativo Sakai (16/11/2007)

Fecha: 16/11/2007

Charlas de los viernes

Una breve introducci�n a los Aspectos Inform�ticas del Entorno de Aprendizaje Colaborativo Sakai para educar, investigar y aprender.

Lic. Alejandro Sartorio

Tem�ticas y Objetivos de la charla:
- Identificar las componentes esenciales de una plataforma e-learning.
- Mostrar en funcionamiento de la plataforma e-learning Sakai.
- Mostrar la arquitectura, tecnolog�as y entornos para el desarrollo del framework Sakai.
- Introducir el concepto de Dispositivo Hipermedial context-aware Din�mico (DHc-aD).
- Mostrar los aportes inform�ticos propuesto en el proyecto Obra Abierta (CONICET - UNR - IMAGE CAMPUS S.R.L)
- Contar una propuesta de evoluci�n desde una Aplicaci�n e-learning a un Dispositivo context-aware Din�mico.
- La teor�a de coordinaci�n de contratos como abstracci�n de las relaciones (alumno-herramienta) con aspectos context-awareness.
- Una metodolog�a para el dise�o de procesos e-learning de un DHc-aD.
- Presentaci�n del proyecto "Ciber" (CCT-Rosario, IRICE y CIFASIS) como una oportunidad para la realizaci�n de una pasant�a para los alumnos de LCC.
- Posible propuestas de Tesina en el marco del proyecto "T�cnicas de Ing. de Software aplicadas al Dispositivo Hipermedial Din�mico" (CIFASIS-UNR).

Horario: Viernes 16 a las 17:10 hs.
Lugar: Aula 22, FCEIA, Pellegrini 250.

Esta ser� la novena de la serie de charlas organizadas por el grupo de estudios que dirige el Dr. Pablo Mart�nez L�pez (Fidel).

Presentaci�n de la tesina de Jorge Sacchini (30/10/2007)

Fecha: 30/10/2007

Presentaci�n de Tesina

T�tulo:
"Un Generador de Condiciones de Verificaci�n Combinado con An�lisis Est�ticos"

Tesista:
Jorge Sacchini

D�a:
Viernes 30 de Octubre

Hora:
14:00hs

Lugar:
Aula 22, FCEIA (Pellegrini 250)

abstract:

Proof-Carrying Code (PCC) establece una arquitectura para la ejecuci�n segura de c�digo m�vil. El productor adjunta al c�digo una prueba que garantiza que el c�digo cumple con una pol�tica de seguridad impuesta por el consumidor. Un generador de condiciones de verificaci�n (VCgen) es un componente de la arquitectura PCC que, al aplicarse a un programa, genera una f�rmula cuya prueba garantiza que el programa satisface la pol�tica de seguridad.
Aplicar un VCgen en un lenguaje con excepciones (como Java bytecode) puede resultar en un gran n�mero de obligaciones de prueba, debido a la gran cantidad de instrucciones con varios sucesores. En este trabajo, presentamos un VCgen para Java bytecode que utiliza an�lisis est�ticos de c�digo para reducir el n�mero de obligaciones de prueba. Como resultado, la tarea de producir una prueba para dichas obligaciones es m�s simple, y los t�rminos de prueba obtenidos son m�s peque�os.
Formalizamos el VCgen en Coq, y probamos que es correcto con respecto a la formalizaci�n Bicolano de la sem�ntica de Java bytecode.

Acto Academia Nacional de Ciencias en nuestra Facultad (26/10/2007)

Fecha: 26/10/2007

La Sesi�n P�blica que realizar� la Academia Nacional de Ciencias Exactas, F�sicas y Naturales en nuestra Facultad, el d�a viernes 26 de octubre a las 11.00 horas, para incorporar al distinguido matem�tico franc�s Dr. Pierre-Louis Lions como Acad�mico Honorario de la misma.

Las notables contribuciones del Dr. Pierre-Louis Lions le valieron ser galardonado en 1994 con la medalla Fields, m�xima distinci�n en la disciplina y equivalente al Premio Nobel en otras �reas.

Cabe se�alar que esta es la primera vez que la Academia de Ciencias realizar� un acto de esta naturaleza fuera de su sede en la ciudad de Buenos Aires.

Luego de la Apertura de la Sesi�n y entrega del diploma de Acreditaci�n, el Acad�mico Correspondiente en Paris-Francia, Dr. Edmundo Rofman presentar� al recipiendario, quien posteriormente disertar� sobre �Analysis, models and simulations�.

A continuaci�n de la Sesi�n nuestra Facultad rendir� "Homenaje al Profesor Dr. Roberto Lisandro Gonz�lez", quien fuera destacado profesor e investigador de la casa y Director del Instituto de Matem�tica Beppo Levi.

Charlas de los viernes - Quitando el sarro de la pava (26/10/2007)

Fecha: 26/10/2007

Charlas de los viernes

Quitando el sarro de la pava

Lic. Andrea Torres

Resumen:
Cuando un programa debe recorrer estructuras de datos construidas a partir de tipos mutuamente recursivos, a menudo la mayor parte del c�digo est� destinada al recorrido de la estructura ocultando entre las l�neas la peque�a parte que realiza en trabajo de inter�s. En el paper Scrap Your Boilerplate: A practical Design Pattern for Generic Programming de Ralf L�mmel y Simon Peyton Jones, se describe una t�cnica que permite que este c�digo que �ensucia� el programa sea escrito de una vez y para siempre dejando al programador concentrarse en la parte importante del algoritmo.

Horario: Viernes 26 a las 18:15 hs.
Lugar: Aula 22, FCEIA, Pellegrini 250.

Esta ser� la octava de la serie de charlas organizadas por el grupo de estudios que dirige el Dr. Pablo Mart�nez L�pez (Fidel).

eXactas.org - Eventos

Symposium on Automatic Program Verification (14/02/2009 - 15/02/2009)

Festival Latinoamericano de Instalaci�n de Software Libre (26/04/2008)

�Qu� es el FLISoL?

�Qui�n organiza el FLISoL?

�A qui�n est� dirigido el evento?

�Cu�nto cuesta la asistencia al evento?

�Qu� beneficios obtengo asistiendo al FLISoL?

�C�mo puedo saber si en mi ciudad se realizar� el evento?

Festival Latinoamericano de Instalaci�n de Software Libre (26/04/2008)

�Qu� es el FLISoL?

�Qui�n organiza el FLISoL?

�A qui�n est� dirigido el evento?

�Cu�nto cuesta la asistencia al evento?

�Qu� beneficios obtengo asistiendo al FLISoL?

�C�mo puedo saber si en mi ciudad se realizar� el evento?

Presentaci�n de Tesina de Pablo Mata (21/12/2007)

Presentaci�n de Tesina

T�tulo: "Flowx: Implementaci�n de No Interferencia en Linux" Tesista: Pablo Mata D�a: Viernes 21 de Diciembre Hora: 12:00hs Lugar: Aula 23, FCEIA (Pellegrini 250)

Presentaci�n de Tesina de Alejandro D�az-Caro (Janus) (21/12/2007)

Presentaci�n de Tesina

T�tulo: "Agregando medici�n al C�lculo de van Tonder" Tesista: Alejandro D�az-Caro D�a: Viernes 21 de Diciembre Hora: 10:45hs Lugar: Aula 23, FCEIA (Pellegrini 250)

Charla "Controlling timing channels in multithreaded programs" (20/12/2007 - 06/12/2007)

Intro al Entorno de Aprendizaje Colaborativo Sakai (16/11/2007)

Charlas de los viernes

Una breve introducci�n a los Aspectos Inform�ticas del Entorno de Aprendizaje Colaborativo Sakai para educar, investigar y aprender.

Lic. Alejandro Sartorio

Presentaci�n de la tesina de Jorge Sacchini (30/10/2007)

Presentaci�n de Tesina

T�tulo: "Un Generador de Condiciones de Verificaci�n Combinado con An�lisis Est�ticos" Tesista: Jorge Sacchini D�a: Viernes 30 de Octubre Hora: 14:00hs Lugar: Aula 22, FCEIA (Pellegrini 250)

Acto Academia Nacional de Ciencias en nuestra Facultad (26/10/2007)

Charlas de los viernes - Quitando el sarro de la pava (26/10/2007)

Charlas de los viernes

Quitando el sarro de la pava

Lic. Andrea Torres

T�tulo:
"Flowx: Implementaci�n de No Interferencia en Linux"

Tesista:
Pablo Mata

D�a:
Viernes 21 de Diciembre

Hora:
12:00hs

Lugar:
Aula 23, FCEIA (Pellegrini 250)

T�tulo:
"Agregando medici�n al C�lculo de van Tonder"

Tesista:
Alejandro D�az-Caro

D�a:
Viernes 21 de Diciembre

Hora:
10:45hs

Lugar:
Aula 23, FCEIA (Pellegrini 250)

T�tulo:
"Un Generador de Condiciones de Verificaci�n Combinado con An�lisis Est�ticos"

Tesista:
Jorge Sacchini

D�a:
Viernes 30 de Octubre

Hora:
14:00hs

Lugar:
Aula 22, FCEIA (Pellegrini 250)