Nie jesteś zalogowany |
Abstrakcyjne podejście do weryfikacji bajtkodu Javy
- Prelegent(ci)
- Patryk Czarnik
- Afiliacja
- Uniwersytet Warszawski
- Termin
- 4 maja 2009 10:15
- Pokój
- p. 4790
- Seminarium
- Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji
Weryfikacja bajtkodu to czynność przeprowadzana przez większość implementacji maszyny wirtualnej Javy podczas ładowania bajtkodu, w celu sprawdzenia poprawności programu przed jego uruchomieniem. W trakcie weryfikacji, w celu sprawdzenia poprawności typowej, przeprowadzana jest m.in. statyczna analiza przepływu danych. Bicolano to formalizacja maszyny wirtualnej oraz semantyki bajtkodu Javy opracowana w ramach projektu Mobius. Pracuję nad formalizacją algorytmu weryfikacji bajtkodu w Coqu, w oparciu o Bicolano. Moja formalizacja ma charakteryzować się tym, że algorytm nie rozpatruje bezpośrednio poszczególnych instrukcji, ale analizuje "sygnatury instrukcji" opisujące na poziomie typów jak instrukcja wpływa na stan. W połączeniu z modularną budową formalizacji, ma to ułatwić analizowanie weryfikacji bajtkodu dla różnych zestawów instrukcji i różnych hierarchii typów. Na seminarium przypomnę ogólniki, przypomnę pomysł sygnatur instrukcji oraz szczegółowo przedstawię formalizację "półkrat dobrze ufundowanych", czym zajmowałem się (razem z Jackiem) ostatnio. Przy okazji będzie coś o klasach w Coqu.
