Redazione RHC : 19 Giugno 2020 10:23
Un team di ricercatori dell’Università del Michigan e Microsoft Research e Carnegie Mellon, ha escogitato un modo per verificare che una classe di programmi complessi sia priva di #bug senza la necessità di #test del #software tradizionale. Chiamato #Armada, il sistema utilizza una tecnica chiamata “verifica formale” per dimostrare se un software produrrà ciò che dovrebbe.
Si rivolge a software che esegue l’esecuzione simultanea, un metodo diffuso per migliorare le prestazioni, che è stato a lungo una caratteristica particolarmente impegnativa per applicare questa tecnica.
I programmi concorrenti sono noti per la loro complessità, ma sono stati uno strumento importante per aumentare le prestazioni dopo che la velocità dei processori ha iniziato a salire.
 CVE Enrichment Mentre la finestra tra divulgazione pubblica di una vulnerabilità e sfruttamento si riduce sempre di più, Red Hot Cyber ha lanciato un servizio pensato per supportare professionisti IT, analisti della sicurezza, aziende e pentester: un sistema di monitoraggio gratuito che mostra le vulnerabilità critiche pubblicate negli ultimi 3 giorni dal database NVD degli Stati Uniti e l'accesso ai loro exploit su GitHub.
Cosa trovi nel servizio: ✅ Visualizzazione immediata delle CVE con filtri per gravità e vendor. ✅ Pagine dedicate per ogni CVE con arricchimento dati (NIST, EPSS, percentile di rischio, stato di sfruttamento CISA KEV). ✅ Link ad articoli di approfondimento ed exploit correlati su GitHub, per ottenere un quadro completo della minaccia. ✅ Funzione di ricerca: inserisci un codice CVE e accedi subito a insight completi e contestualizzati.
Se ti piacciono le novità e gli articoli riportati su di Red Hot Cyber, iscriviti immediatamente alla newsletter settimanale per non perdere nessun articolo. La newsletter generalmente viene inviata ai nostri lettori ad inizio settimana, indicativamente di lunedì. |
La verifica formale, è un mezzo per dimostrare che un programma produrrà sempre valori corretti senza doverlo testare con una gamma completa di possibili input.
Ragionando sul programma come una prova matematica, i programmatori possono dimostrare che bug o errori sono impossibili e che la sua esecuzione è ermetica. Questo supera il difetto comune a tutti i programmi, anche senza concorrenza, che testare qualcosa in modo esauriente può essere impraticabile o effettivamente impossibile.
Ovviamente non si parla di bug di sicurezza.
#redhotcyber #cybersecurity #amanda #metodologia
https://techxplore.com/news/2020-06-method-complex-bug-free.amp
RedazioneIl 18 novembre 2025, alle 11:20 UTC, una parte significativa dell’infrastruttura globale di Cloudflare ha improvvisamente cessato di instradare correttamente il traffico Internet, mostrando a milion...
Questo è il quinto di una serie di articoli dedicati all’analisi della violenza di genere nel contesto digitale, in coincidenza con la Giornata Internazionale per l’Eliminazione della Violenza co...
18 novembre 2025 – Dopo ore di malfunzionamenti diffusi, l’incidente che ha colpito la rete globale di Cloudflare sembra finalmente vicino alla risoluzione. L’azienda ha comunicato di aver imple...
La mattinata del 18 novembre 2025 sarà ricordata come uno dei blackout più anomali e diffusi della rete Cloudflare degli ultimi mesi. La CDN – cuore pulsante di milioni di siti web, applicazioni e...
La stanza è la solita: luci tenui, sedie in cerchio, termos di tisane ormai diventate fredde da quanto tutti parlano e si sfogano. Siamo gli Shakerati Anonimi, un gruppo di persone che non avrebbe ma...
