Towards a type-based analysis of real PKCS#11 devices