Abstrakcyjne podejście do weryfikacji bajtkodu Javy

Speaker(s)

Patryk Czarnik

Affiliation

Uniwersytet Warszawski

Date

May 4, 2009, 10:15 a.m.

Room

room 4790

Seminar

Seminar Semantics, Logic, Verification and its Applications

---

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.

---