{"id":5445,"date":"2016-02-23T13:14:46","date_gmt":"2016-02-23T11:14:46","guid":{"rendered":"http:\/\/www.ftf.or.at\/?p=5445"},"modified":"2016-02-23T13:14:46","modified_gmt":"2016-02-23T11:14:46","slug":"behaviorally-reliable-secure-and-resilient-application-software","status":"publish","type":"post","link":"https:\/\/www.ftf.or.at\/?p=5445","title":{"rendered":"Behaviorally Reliable, Secure and Resilient Application Software"},"content":{"rendered":"

Muhammad Taimoor Khan, MSc. PhD. | 29.02.2016 | 11:00 Uhr | E.2.69<\/strong><\/p>\n

Abstract<\/strong><\/p>\n

In this talk, we present a rigorous behavior based approach to develop reliable, secure and resilient application software for industrial control systems (in particular). The goal here is to employ formal methods to \ufb01rst build application right and then to continuously monitor the application for security and resilience.
\nTo achieve the goal, we \ufb01rst develop correct-and-secure-by-construction application software using theorem proving (i.e. prover Coq) through re\ufb01nement and synthesis of abstract data types. Then we introduce a run-time security monitor for application software, which detects both known and unknown computational cyber attacks. For resilience, we employ dependency directed reasoning to recover the system in a safe state, if any inconsistency is detected. Our security monitor is sound and complete, eliminating false alarms, as well as e\ufb03cient, supporting real-time systems. In contrast, conventional run-time security monitors for application software either produce (high rates of) false alarms (e.g. intrusion detection systems) or limit application performance (e.g. run-time veri\ufb01cation systems).
\nOur run-time monitor detects attacks by checking the consistency between the application run-time behavior and its expected behavior modeled in its speci\ufb01cation. Our speci\ufb01cation language is based on monadic second order logic (i.e. \ufb01rst order logic and set theory) and event calculus interpreted over algebraic data structures; application implementation can be in any programming language. Based on our de\ufb01ned denotational semantics of the speci\ufb01cation language, we prove that the security monitor is sound and complete, i.e. it produces an alarm if and only if it detects an inconsistency between the application execution and the speci\ufb01ed behavior. Importantly, the monitor detects not only cyberattacks but all behavioral deviations from speci\ufb01cation, e.g. bugs, and so, is readily applicable to the security of legacy systems.
\nFinally, we present the evaluation of the monitor in the industrial control systems security domain, speci\ufb01cally in water management, demonstrating that run-time, sound and complete monitors employing veri\ufb01cation techniques are e\ufb00ective, e\ufb03cient and readily applicable to demanding real-time critical systems, without scalability limitations.<\/p>\n

\"Khan\"<\/a>Muhammad Taimoor Khan<\/strong> is a postdoctoral researcher at Qatar Computing Research Institute (jointly with CSAIL, MIT, USA), Qatar. His current research is to develop reliable, secure and resilient software by the application of formal methods. On one hand, his project is focused on developing a tool to automatically detect and correct, known and unknown attacks through monitoring behavioral inconsistencies between specification and execution at run-time. On the other hand, his another project is focused on using theorem prover as a programming language to develop correct-and-secure-by construction software.
\nPrior to this, Taimoor Khan has passed doctoral studies at Research Institute for Symbolic Computation, Hagenberg, Austria with All-Distinctions in 2014. His PhD dissertation was about formal specification and verification of computer algebra software. Before joining RISC, he graduated in MSc Advanced Distributed Systems from the University of Leicester, UK with Distinction in 2008. As a final semester project he worked on the model-based verification of the various communication protocols of NASA in the frame of project \u201cSpace Link Extension Service Management\u201d. Also prior to this, he completed his M.Sc. in Computer Science from Pakistan in 2001 and then worked for about five years in the software industry specializing in Java (EE\/ME), XML and Web Services.
\nTaimoor Khan has been visiting scientist at various international reputed institutes including CSAIL, MIT, USA and ENSIIE, INRIA, France. Also he has won various research awards including the best student paper award at the most premier conference in computer algebra (CICM) in 2012.
\nHe is also working as an associate tutor at University of Leicester, UK. Here he is teaching different courses (e.g. Domain Specific Languages) to MSc students (DL) and supervising their final semester projects. Prior to that, he has also taught undergraduate and graduate students at numerous universities in Pakistan as an assistant professor for several years.<\/p>\n

 <\/p>\n","protected":false},"excerpt":{"rendered":"

Muhammad Taimoor Khan, MSc. PhD. | 29.02.2016 | 11:00 Uhr | E.2.69 Abstract In this talk, we present a rigorous behavior based approach to develop reliable, secure and resilient application software for industrial control systems (in particular). The goal here … Continue reading →<\/span><\/a><\/p>\n","protected":false},"author":20,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"sfsi_plus_gutenberg_text_before_share":"","sfsi_plus_gutenberg_show_text_before_share":"","sfsi_plus_gutenberg_icon_type":"","sfsi_plus_gutenberg_icon_alignemt":"","sfsi_plus_gutenburg_max_per_row":"","footnotes":""},"categories":[1],"tags":[],"class_list":["post-5445","post","type-post","status-publish","format-standard","hentry","category-tewi-kolloquium"],"_links":{"self":[{"href":"https:\/\/www.ftf.or.at\/index.php?rest_route=\/wp\/v2\/posts\/5445","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.ftf.or.at\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.ftf.or.at\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.ftf.or.at\/index.php?rest_route=\/wp\/v2\/users\/20"}],"replies":[{"embeddable":true,"href":"https:\/\/www.ftf.or.at\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=5445"}],"version-history":[{"count":13,"href":"https:\/\/www.ftf.or.at\/index.php?rest_route=\/wp\/v2\/posts\/5445\/revisions"}],"predecessor-version":[{"id":5460,"href":"https:\/\/www.ftf.or.at\/index.php?rest_route=\/wp\/v2\/posts\/5445\/revisions\/5460"}],"wp:attachment":[{"href":"https:\/\/www.ftf.or.at\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=5445"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.ftf.or.at\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=5445"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.ftf.or.at\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=5445"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}