Sono nuovo nell'arena dei metodi formali, ma sento di avere una conoscenza approfondita delle sue applicazioni. Tuttavia, mi sembra di incontrare solo metodi formali applicati al processo di sviluppo, in quanto il software è stato creato.
Mi piacerebbe essere in grado di applicare metodi formali sul software esistente per verificare se aderisce ai controlli di accesso basati sui ruoli (RBAC) e alla separazione delle informazioni sensibili seguendo il metodo Bell-LaPadula (BLP).
Quali metodi e strumenti sai che offrono una soluzione automatizzata per la verifica RBAC e BLP del software / codice sorgente esistente?