Supervisor's Name: Brigitte Pientka
Supervisor's Email: bpientka [at] cs.mcgill.ca
Supervisor's Phone: 398 2583
Supervisor's Website: http://www.cs.mcgill.ca/~bpientka/
Supervisor's department: Computer Science
Course number: COMP 396 (Computer Science)
Term: Summer 2014
Project start date: 1 May
Project end date: 31 August
Project title: Specifying linear authorization policies in Celf
Project description (50-100 words suggested): Celf is a tool for experimenting with deductive and concurrent systems prevalent in programming languages, security protocols and authorization policies. It directly supports reasoning with consumable resources. In this project, we use Celf to encode and specify a linear authorization logic which treats consumable resources such as single-use authorization. In particular, we will study and encode two case studies: 1) a student registration system which satisfies different constraints (for example it prevents students to register only once for a course, one cannot register for a course a student has already passed, etc.) and 2) Online Banking system. The goal is to understand the benefits and challenges in using a rich logical framework such as Celf for these applications.
Prerequisite: 1 term completed at McGill + CGPA of 3.0 or higher; or permission of instructor.
Grading scheme (The final report must be worth at least 50% of final grade): Final oral presentation 15%, final written report 55%, prototype specification 15%, 15% participation in discussion and joint meetings (including weekly lab meetings).
Project status: This project is taken. The professor has no more '396' projects this term.
How students can apply / Next steps: Bring a printed copy of this application form and your advising transcript to me during office hours.
Ethics, safety, and training: Supervisors are responsible for the ethics and safety compliance of undergraduate students. This project involves NEITHER animal subjects, nor human subjects, nor biohazardous substances, nor radioactive materials, nor handling chemicals, nor using lasers.