Description: http://data.proidea.org.pl/confidence/9edycja/materialy/prezentacje/AdreasBogk.pdf
The talk is divided into three sections. The first section will illustrate the source of many of the vulnerabilities encountered in daily practice, and why current technological approach fails to address these in a systematic manner. I.ll be arguing that the correct approach to get rid of many classes of vulnerabilities lies within recent progress in theoretic computer science, which needs to be applied to practice.
The second part will look into three different real world projects that utilize mechanisms of formal verification. I.ll look at them in terms of engineering, i.e., do those approaches represent something that can be scaled to arbitrary projects? The different approaches demonstrated and the respective projects are SMT solvers (MS Hyper-V), post facto verification using Isabell/HOL (verified L4), and integrated development using Coq (CompCert).
The third part of the talk will give an outlook into future computer architectures, which will allow to show security guarantees for a lot of real world demands. This is not just about avoiding exploitable vulnerabilities, but also about verified enforcement of role-based access control and provenance-based enforcement of information flow throughout the whole system.
Tags: securitytube , Confidence , hacking , hackers , information security , convention , computer security , Confidence 11 , Confidence-2011 ,
Disclaimer: We are a infosec video aggregator and this video is linked from an external website. The original author may be different from the user re-posting/linking it here. Please do not assume the authors to be same without verifying.