Specifying linear authorization policies in Celf - COMP 396 Undergraduate Research Project Application Form
INSTRUCTIONS - PROFESSORS: Please print and review this form. Complete or correct the sections, as applicable, from "Supervisor's Name" to "Ethics, safety, and training". Please sign and date near the bottom ("Supervisor's signature").
INSTRUCTIONS - STUDENTS: You may receive this form by email, or you may download it after it has been posted here. Either way, print and review this form. Complete or correct the sections, from "Student's Name" to "Student's Level", and sign ("Student signature"). Ask your supervisor to sign her/his section near the bottom. Take it to the department* corresponding to the course number in Section A; this may or may not be your own department. (* EXCEPTIONS: For NSCI 396 and COGS 396, please bring it to the Interdisciplinary Programs Adviser in Dawson Hall.) Do not register for a '396' course on Minerva until you receive departmental permission. Have a discussion with your supervisor about time/work expectations, keeping in mind that this is a 3-credit course (roughly, 10 hours per week for 12 weeks). Remember that a '396' course is an elective.
INSTRUCTIONS - DEPARTMENTS: After the unit chair/director/designate approves (or not) this project, please notify student. If approved, please give student permission to register on Minerva, and send a copy of this form (with signatures) to the Office for Undergraduate Research in Science (either fax, or internal mail to Dawson Hall 408-A, or PDF scan + email).
QUESTIONS OR FEEDBACK? Contact the Office for Undergraduate Research in Science.
Supervisor's Name: Brigitte Pientka
Supervisor's Email: bpientka [at] cs [dot] mcgill [dot] 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.