COMP3008 2020–21 – D. Karapetyan – Coursework (file version 1.2) Page 1 1 Introduction You will develop a solver for the Workflow Satisfiability Problem. Please note the difference between the problem and the problem instance (or simply instance). Problem (in our case, the Workflow Satisfiability Problem) is a generic description of a family of mathematical questions. Problem instance is a specific mathematical question, with specific parameters, constraints, etc. Your solver needs to do the following: 1. Read the problem instance from a file. The file name is passed to the solver as the first and only command line parameter. (If you implement additional features, you can introduce more command line parameters.) 2. Establish if the problem instance is satisfiable or unsatisfiable. 3. Measure the time taken by Step 2 and print it in milliseconds 4. If the problem instance is unsatisfiable: • Print ‘unsat’. 5. If the problem instance is satisfiable: • Print ‘sat’; • Print a solution that satisfies the problem. instance • Check if this solution is the only solution to the problem instance; print ‘this is the only solution’ if this is the only solution and ‘other solutions exist’ if there exist other solutions. You can use any programming language to implement your solver, e.g. Python, Java or C#, however your solver has to be based on OR Tools or Z3. It should be possible to run your solver on the UoN Virtual Desktop. If in doubt about the choice of language or libraries, talk to the module convenor. 2 Workflow Satisfiability Problem Workflow Satisfiability Problem is an important problem in access control (in- formation security). It is about organising a workflow in an organisation in such a way that certain security-related constraints are satisfied. You are given a set U of employees, or users, and a set S of tasks, or steps (e.g., a task could be to check a contract, or to sign it, or to send it to the client). The problem is to find an assignment pi : S → U of users to steps such that all the constraints are COMP3008 2020–21 – D. Karapetyan – Coursework (file version 1.2) Page 2 satisfied. (Note that every step has to be assigned exactly one user; a user may be assigned one or several steps, or may not be assigned any steps.) The constraints can be of the following types: • Authorisations: a user can only be assigned steps that they are authorised for; for example, an employee may not be qualified to check a contract, and hence will not be authorised for the corresponding step. If authori- sations are not specified for a user, that user can be assigned any steps. Authorisations can be specified at most once for each user. Formal definition: Given: a user u ∈ U and an authorisation list A ⊆ S. Requirement: if pi(s) = u for some s ∈ S then s ∈ A. • Separation of duty: for a given pair of tasks, ensure that they are as- signed to two different employees; for example, if a contract requires two signatures, those signatures have to come from two different people Formal definition: Given: a pair of steps s′ 6= s′′ ∈ S. Requirement: pi(s′) 6= pi(s′′). • Binding of duty: for a given pair of tasks, ensure that they are assigned the same employee; for example, the person responsible for checking a contract should also sign that contract. Formal definition: Given: a pair of steps s′ 6= s′′ ∈ S. Requirement: pi(s′) = pi(s′′). When you read this document for the first time, I suggest that you skip the rest of the constraints. • At-most-k: for a given set of steps T ⊆ S, ensure that at most k users are assigned to steps T . For example, when several tasks are associated with a piece of sensitive information, it is good to keep the number of people having access to it to a minimum. Formal definition: Given: a set of steps T ⊆ S and a positive integer k ≤ |S|. Requirement: |{pi(s) : s ∈ T}| ≤ k. • One-team constraint: for a given set of steps and a list of teams, ensure that all these steps are assigned to members of one team. Formal definition: Given: a set of steps T ⊆ S; given a set of teams U1, U2, . . . , Ur, where Ur ⊆ U for i = 1, 2, . . . , r and Ui ∩ Uj = ∅ for every i 6= j ∈ {1, 2, . . . , r}. Requirement: {pi(s) : s ∈ T} ⊆ Ui for some i ∈ {1, 2, . . . , r}. COMP3008 2020–21 – D. Karapetyan – Coursework (file version 1.2) Page 3 Example of a problem instance with four users U = {u1, u2, u3, u4}, three steps S = {s1, s2, s3} and six constraints: 1. Authorisations: u = u1 and A = {s1, s2}. 2. Authorisations: u = u2 and A = {s3}. 3. Authorisations: u = u4 and A = {s3}. 4. Binding of duty: s′ = s1, s′′ = s3. 5. Separation of duty: s′ = s1, s′′ = s2. 6. Separation of duty: s′ = s2, s′′ = s3. Solution: pi(s1) = u3, pi(s2) = u1, pi(s3) = u3. In fact, this is the only solution to this problem instance. 3 Input file format The input data will be provided in text files. The file begins with a header of the following format: #Steps: 3 #Users: 4 #Constraints: 6 Steps are referred to as sX, where X is the index of the step. In the above example, the problem instance has three steps: s1, s2 and s3. Indexing begins with 1. Similarly, users are referred to as uX, where X is the index of the user. In the above example, the problem instance has four users: u1, u2, u3 and u4. The header is followed by c lines, where c is the number of constraints given in the header (six in this example). Each line defines exactly one constraint. Each constraint line begins with the constraint name, followed by parameters. The parameters of each constraint are explained below. • Example of an authorisations constraint: Authorisations u1 s1 s2 COMP3008 2020–21 – D. Karapetyan – Coursework (file version 1.2) Page 4 This defines an authorisations constraint for u = u1 and A = {s1, s2} The list of steps can be empty, e.g. Authorisations u1 This means that u1 is not authorised for any steps. • Example of a binding-of-duty constraint: Binding-of-duty s1 s3 This defines a binding-of-duty constraint for s′ = s1, s′′ = s3. • Example of a separation-of-duty constraint: Separation-of-duty s1 s2 This defines a separation-of-duty constraint for s′ = s1, s′′ = s2. • Example of an at-most-k constraint: At-most-k 2 s1 s2 s3 This defines an at-most-k constraint for k = 2 and T = {s1, s2, s3}. • Example of a one-team constraint: One-team s1 s2 s4 (u1 u2) (u5 u7 u8) (u3) This defines a one-team constraint for T = {s1, s2, s4} and r = 3 teams U1 = {u1, u2}, U2 = {u5, u7, u8} and U3 = {u3}. Each team has to include at least one user, and the set of steps has to include at least one step. The number of teams can be anything from 1 to |U |. The format is not case-sensitive, e.g. it is legal to write Authorisations or authorisations. Extra spaces between words, numbers etc. should be ig- nored when reading the file, e.g. it is legal to define a constraint as follows: Authorisations u1 s1 s2. You can assume that the input file is correctly formatted. The following file describes the instance given in Section 2. COMP3008 2020–21 – D. Karapetyan – Coursework (file version 1.2) Page 5 #Steps: 3 #Users: 4 #Constraints: 6 Authorisations u1 s1 s2 Authorisations u2 s3 Authorisations u4 s3 Binding-of-duty s1 s3 Separation-of-duty s1 s2 Separation-of-duty s2 s3 You can find this instance in file example3.txt. The samples instances can be downloaded at https://moodle.nottingham.ac.uk/mod/resource/view.php?id=4765333 List of the main sample instances: # Auth. BOD SOD At-most-k One-team Sat Unique Example 1 Example 2 Example 3 Example 4 Example 5 Example 6 Example 7 Example 8 Example 9 Example 10 Example 11 Example 12 Example 13 Example 14 Example 15 Example 16 Example 17 Example 18 Example 19 The columns of the table are as follows (from left to right): COMP3008 2020–21 – D. Karapetyan – Coursework (file version 1.2) Page 6 • Instance name • Whether it includes authorisation constraints • Whether it includes binding-of-duty constraints • Whether it includes separation-of-duty constraints • Whether it
includes at-most-k constraints • Whether it includes one-team constraints • Whether it is satisfiable • Whether there exists exactly one solution Examples 1–8 are small and good for debugging. Examples 9–15 are relatively large and good for testing. Examples 16–19 are large and good for performance analysis (in my experiments, solving each of them tool in the order of 5–10 sec). In addition to these instances, you can use the instances in folders ‘3-constraint’, ‘4-constraint’ and ‘5-constraint’. Instances in each of these folders share similar properties and thus are good for empirical analysis of your solver. 4 Report The report has to include the following sections: • Introduction. Keep it brief. You do not have to describe the problem; instead, you can reference this document. Here is a good place to discuss what solver and language you chose, which parts of the coursework you did, whether you know of any functionality that does not (always) work, etc. If you researched the workflow satisfiability literature, discuss this here (possibly leaving details until next section). • Formulation of the problem. You can find examples of such formulations in lab sheets. While mathematical formulation is usually more abstract than the actual implementation, your formulation has to be detailed enough so that it is clear how it can be implemented in OR-Tools/Z3. If you introduced any new notations, be clear about them. You can split the formulation into several parts: e.g., the part that is unre- lated to the constraints and then the formulation for each constraint type. Unless obvious, explain for each constraint type why your formulation is correct and what API functions you use. COMP3008 2020–21 – D. Karapetyan – Coursework (file version 1.2) Page 7 • Implementation. Explain here how to compile/execute your solver. Also explain the logic of work of your solver; specifically, how does it establish if there exist multiple solutions to the problem? Discuss any known bugs. If your implementation is straightforward, this section is likely to be very short. • Evaluation. For each of the sample instances, report if your solver tackles it correctly and how long does this take. You can add more performance analysis here if you like. • Conclusions. Discuss the strengths and weaknesses of your solver. Discuss ways to improve it if you have any ideas. You do not have to follow exactly this structure but this is a reasonable template. 5 Submission The submission is in Moodle. You will have to submit the following files: • The report in .docx or .pdf format • The code of your solver; for example, if your code is in Python, you will need to submit the .py files In submitting your work, you declare that it is all your own, except where otherwise explicitly indicated. 6 Interview The interview does not affect the mark, however it is a compulsory part of the coursework. Failing to attend the interview will result in mark 0 for the coursework. There will be significant flexibility in choosing the time of the interview. Details will be communicated closer to the submission deadline. The interview will take around 15 minutes and will be conducted via MS Teams. During the interview, you will share your screen to demonstrate how your solver works and to answer questions related to your code and report. You will also be given oral feedback. COMP3008 2020–21 – D. Karapetyan – Coursework (file version 1.2) Page 8 7 Marking criteria Criterion Weight The solution approach (judged from the code and the report) 30% Correctness and quality of the program and source code 20% Performance of the solver; analysis of the performance 20% Quality of the report (how easy it is to follow, how precise it is, how accurately does it describe the solution method, referenc- ing, how well it is written and formatted) 30% You are allowed to reuse publicly available code and/or formulations (subject to correct referencing), however your mark will reflect only your own contributions. This should not discourage you from utilising the advanced techniques from the literature; understanding of the scientific literature will positively affect your mark. If in doubt, talk to the module convenor. If you struggle with the implementation, you may still achieve a reasonable mark for the report. 8 Grading guidelines Above 79 The program and the report exceed expectations; for example, extra functionality is implemented, interesting analysis is per- formed, etc. 70–79 All the requirements are met: the solver performs as expected and the report adequately reflects the work. 60–69 Most of the requirements are met: the solver mostly performs as expected and the report adequately reflects the work, possibly with minor weaknesses. 50–59 The core requirements are met, possibly with minor weaknesses. 40–49 The core requirements are met, with major weaknesses. Below 40 The core requirements are not met. 9 Further information If you have questions, talk to the module convenor. COMP3008 2020–21 – D. Karapetyan – Coursework (file version 1.2) Page 9 There will be a Q&A session about the coursework on 26 Nov at 12.00. Finally, an FAQ will be maintained at https://moodle.nottingham.ac.uk/ mod/page/view.php?id=4763758 10 Academic misconduct You are allowed to use any publicly available sources as long as you correctly reference them. The rules of academic misconduct are detailed in • The Computer Science UG/PGT handbook available from the Moodle Community page • The academic misconduct policy document: https://www.nottingham. ac.uk/qualitymanual/assessment-awards-and-deg-classification/ pol-academic-misconduct.aspx 欢迎咨询51作业君
