Strumenti automatici per l'applicazione di metodi formali per la verifica della politica di sicurezza nel software esistente

1

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?

    
posta Methmal Forods 14.06.2015 - 17:00
fonte

1 risposta

0

Ha scritto su metodi formali e sicurezza molti anni fa qui - link - le basi su cui è come applicare gli standard Orange Book della vecchia scuola al software moderno.

Se dovessi riscrivere quel post nel 2015, alcuni degli aggiornamenti che aggiungerei sono che i controllori di modelli basati su SMT sono diventati molto più diversi, integrati e avanzati rispetto a quelli semplici che ho delineato (SPIN e JPF ). Queste pagine dovrebbero indirizzarti verso alcuni di questi progressi: link - link - link

DARPA sta lavorando a un progetto per la verifica formale della crowd-sourcing (CSFV) qui - link

Anche se sono a favore dell'automazione, sarebbe interessante ascoltare di più sul dominio del problema per formulare raccomandazioni secondarie in merito ai test manuali. È questo per i problemi di autorizzazione di web e di e-commerce web? Quali domini sono coinvolti?

    
risposta data 14.06.2015 - 18:01
fonte

Leggi altre domande sui tag