Abstrakt. Sun och CERT rekommenderar för säker Java-utveckling att inte tillåta delvis initierade objekt att nås. Cert anser att de risker som inte följer denna rekommendation är så allvarliga. Den lösning som för närvarande används för att genomdriva objektet initiering är att genomföra en kodning mönster föreslås av Sun, som inte är formellt kontrolleras. Vi föreslår ett modulärt typsystem för att formellt specificera initieringspolicyn för bibliotek eller program och en typkontroll för att statiskt kontrollera vid belastningstidpunkten att alla laddade klasser respekterar policyn. Detta gör det möjligt att bevisa frånvaron av buggar som har tillåtit några berömda utökningar av privilegier i Java. Våra experimentella resultat visar att vår säkra standardpolicy gör det möjligt att bevisa 91% av klasserna java.lang, java.security och javax.security säker utan annotering och genom att lägga till 57 enkla annoteringar bevisade vi alla klasser utom fyra säkra. Typsystemet och dess ljudstyrka teorem har formaliserats och maskinen kontrolleras med Coq.
Rawtypes REF är ett tillvägagångssätt baserat på ett typsystem för att genomdriva korrekt initiering av objekt i Java.
Enforcing Secure Object Initialization in Java
{'venue': '15th European Symposium on Research in Computer Security (ESORICS) 6345 (2010) 101-115', 'journal': None, 'mag_field_of_study': ['Computer Science']}