Back close
Admissions

Course Detail

Course Name Formal Methods for Security
Course Code 24CY752
Program M. Tech. in Cyber Security
Credits 3
Campus Coimbatore

Syllabus

Syllabus

Formal Methods – Propositional and Predicate logic, and theorem-proving, Fixed-points and their role in program analysis and model-checking, Verification of sequential programs using weakest preconditions and inductive methods, and verification of concurrent and reactive programs/systems using model- checking and propositional temporal logic (CTL and LTL), Application of static and dynamic program analysis and model-checking for detecting common security vulnerabilities in programs and communication protocols, Information flow and taint analysis for security of web applications, pi-calculus for formal modelling of mobile systems and their security. SPIN, PVS, TAMARIN, Frama-C and Isabelle tools. 

Objectives and Outcomes

Prerequisite

Logic and Discrete Mathematics

 

Course Outcome
 

Course Outcome  

Bloom’s Taxonomy Level  

CO 1  

Introduction to Formal Methods- Logic and Program Verification. 

L1  

CO 2  

Understand Temporal Logic and Model Checking for program verifications. 

L2  

CO 3  

Verification of concurrent and reactive programs/systems using model-checking and propositional temporal logic. 

L4  

CO 4  

Application of static and dynamic program analysis and model- checking for detecting common security vulnerabilities in programs and communication protocols 

L3  

CO 5  

Familiarizing SPIN, PVS, TAMARIN, Frama-C and Isabelle tools. 

L5  
 
CO-PO Mapping

CO-PO Mapping  

CO/PO  

PO 1 

PO 2 

PO 3 

PO 4 

PO 5 

PO 6 

PO 7 

PO 8 

PO 9 

PO 10 

PSO1 

PSO2 

PSO3 

CO 1 

1 

2 

3 

2 

3 

1 

– 

1 

1 

– 

0 

0 

0 

CO 2 

1 

2 

3 

2 

3 

1 

– 

1 

1 

– 

1 

1 

1 

CO 3 

1 

2 

3 

2 

3 

1 

– 

1 

1 

– 

2 

2 

2 

CO 4 

1 

2 

3 

2 

3 

1 

– 

1 

1 

– 

2 

2 

2 

CO 5 

1 

2 

3 

2 

3 

1 

– 

1 

1 

– 

2 

2 

2 

Text Books / References

  1. Edmund M. Clarke, Orna Grumberg and Doron Peled, Model Checking , MIT Press, 1999. 
  2. Lloyd, J.W., Logic and Learning: Knowledge Representation, Computation and Learning in Higher-order Logic , Springer Berlin Heidelberg, 2003. 
  3. M. Ruth and M. Ryan, Logic in Computer Science – Modelling and Reasoning about Systems , Cambridge University Press, 2004 . 
  4. G. Bella, Formal Correctness of Security Protocols , Springer, 2009. 
  5. Datta A, Jha S, Li N, Melski D and Reps T, Analysis Techniques for Information Security , Synthesis Lectures on Information Security, Privacy, and Trust, 2010. 

DISCLAIMER: The appearance of external links on this web site does not constitute endorsement by the School of Biotechnology/Amrita Vishwa Vidyapeetham or the information, products or services contained therein. For other than authorized activities, the Amrita Vishwa Vidyapeetham does not exercise any editorial control over the information you may find at these locations. These links are provided consistent with the stated purpose of this web site.

Admissions Apply Now