Functional Verification

Garantire la sicurezza dei dispositivi IoT, medici e elettronici con la Verifica Formale

on 2 Dicembre 2019

La sicurezza dei dispositivi IoT, medici e elettronici in generale è oggi una delle preoccupazioni principali in ambito tecnologico. Tale sicurezza può essere garantita in modo veramente efficace solo se si interviene nella zona più “profonda” dei dispositivi, cioè a livello IC.

Quali sono i problemi di sicurezza dei dispositivi

Ci sono alcuni ambiti d’uso nei quali il problema della sicurezza dei dispositivi è particolarmente sentito:

  • Nell’automotive, i bus per lo scambio interno dei dati possono essere soggetti a manomissioni dall’esterno.
  • In ambito medicale, la maggior parte dei dispositivi – sia fissi sia indossabili – sono sorprendentemente “aperti” nei confronti di possibili manomissioni.
  • I vari sistemi di pagamento – dai POS ai wallet dei telefoni – spesso sono molto vulnerabili rispetto alla diffusione di dati personali.
  • I dispositivi IoT per la domotica – come ad esempio i termostati – in genere non sono attrezzati per controllare eventuali file “infetti” al proprio interno.
  • I monitor dei computer oggi possono essere spiati senza neanche bisogno di passare dal PC, come risulta da un recente studio.

Scarica l’eBook di Mentor sulle App per la Verifica Formale

``Introduction to Automated Formal Apps``

La sicurezza dei dispositivi viene garantita a livello di IC?

Molto spesso i problemi di sicurezza dei dispositivi nascono proprio a livello IC. L’ultimo Functional Verification Study del Wilson Research Group ha evidenziato come le caratteristiche di sicurezza siano implementate solo nel 60% dei progetti ASIC e nel 48% dei progetti FPGA.

Eppure sappiamo che nell’hardware digitale è importante garantire una Root-of-Trust (RoT). Si tratta di un insieme di funzioni considerato attendibile dal sistema operativo del dispositivo e che funge da motore di calcolo separato che controlla il processore crittografico del dispositivo.

Questo schema mostra l’importanza di garantire la sicurezza al livello più basso dello stack.

sicurezza dispositivi

La sicurezza dei dispositivi viene garantita da chiavi private, che a loro volta devono essere protette all’interno dell’hardware di archiviazione.

Gli attuali metodi per garantire la sicurezza dei dispositivi

Le sfide da affrontare per la sicurezza dei dispositivi sono la confidenzialità, cioè la limitazione degli accessi dall’esterno, e l’integrità, ovvero l’affidabilità e accuratezza delle informazioni.

Le tecniche più popolari fin qui usate per garantirle si sono rivelate inefficaci: oscuramento fisico tramite l’involucro, white hat hacking, ispezione, test diretti, constrained-random verification. Il problema è che queste metodologie non sono scalabili al crescere della complessità del circuito.

La soluzione: la verifica formale

La verifica formale è un metodo che utilizza metodi formali matematici per dimostrare o confutare che determinati requisiti o proprietà formali siano stati rispettati. La base matematica del metodo ne garantisce l’esaustività. Essa necessità però di passare all’uso di strumenti specializzati.

Questa Secure Check è la soluzione completamente automatizzata di Mentor e Siemens che consente di gestire la verifica formale. Con Questa Secure Check è possibile verificare in modo esaustivo che solo i percorsi specificati possono raggiungere elementi di sicurezza o di archiviazione critici, ovvero dimostrare formalmente l’intangibilità della “Root-of-Trust” del dispositivo.

questa secure checkDopo che l’utente ha specificato l’archiviazione sicura e i segnali, Questa Secure Check individua automaticamente gli input delle porte e dei modelli black box, generando le proprietà per la confidenzialità e l’integrità. Essa poi verifica formalmente tali proprietà. Le forme d’onda nel pannello di visualizzazione della app evidenziano quali sono i percorsi non sicuri. In tal modo è possibile andare veramente alla radice dei problemi di sicurezza.

Forma Verification

Ebook

Introduction to Automated Formal Apps

Una “app formale” è uno strumento formale o una metodologia ben documentata incentrata su una sfida di verifica specifica e di alto valore. Tale sfida viene risolta in modo più efficiente usando metodi formali che usando approcci basati sulla simulazione. La necessità di creare proprietà o avere conoscenze in Verifica Basata sulle Asserzioni è significativamente ridotta o addirittura completamente eliminata.

Leggendo questo ebook potrai imparare come funziona la verifica formale con gli strumenti messa a disposizione da Questa.

Leggi tutto...
CadlogGarantire la sicurezza dei dispositivi IoT, medici e elettronici con la Verifica Formale