Special Topics EECS 598
Popular in Course
Popular in Engineering Computer Science
This 3 page Class Notes was uploaded by Ophelia Ritchie on Thursday October 29, 2015. The Class Notes belongs to EECS 598 at University of Michigan taught by Staff in Fall. Since its upload, it has received 10 views. For similar materials see /class/231541/eecs-598-university-of-michigan in Engineering Computer Science at University of Michigan.
Reviews for Special Topics
Report this Material
What is Karma?
Karma is the currency of StudySoup.
You can buy or earn more Karma at anytime and redeem it for class notes, study guides, flashcards, and more!
Date Created: 10/29/15
EECS 598 Paper Review by Kien Yue Kuo MOPS an Infrastructure for Examining Security Properties of Software By Hao Chen amp David Wagner This paper presents MOPS a formal approach for nding bugs in securityrelevant software and verifying their absence The idea behind MOPS is to map the security property to a Finite State Automaton and the program as a Pushdown Automaton MOPS then use model checking to determine whether certain states representing violation of the security property in the FSA are reachable in the PDA One advantage of MOPS is that it llly supports interprocedural analysis as opposed to local analysis which only keeps track of states and variables in a single procedure This is useful as shown in the example where drop jrivilegeo forgets to drop privilege in case of error and return to the main lnction which then calls execlO Using PDA to model the program has its pros and cons Since there are efficient algorithms to compute the intersections of a PDA and an FSA and by approximating the program traces which is in general an uncomputable set thus making deciding whether the two languages intersection is null undecidable to a context free language the problem becomes decidable However this also means that some imprecision is introduced by approximating the program trace to a PDA This can be attributed to the fact that data ow is not modeled the checker will go into paths that are infeasible and report them as errors MOPS has the property that it is sound 7 it will make mistakes by making false alarms but will not overlook a real violation This can be very useful when doing an audit but for general debugging purpose having a lot of false positives will limit its usefulness for the programmer will not have the patience to look though say a hundred false positives to find a real error The paper did not give sample numbers of the ratio of real errors to false alarms so it is not obvious how useful MOPS is when used in real applications In contrast the metalevel compilation paper gave solid numbers on the number of false positives and the number of real errors found If the MOPS paper also present these data say with the result of nding the vulnerability in wu ftpd 24 beta 11 it will give readers a better picture of how useful the software is As for the data ow insensitive problem the authors suggest doing a rudimentary data ow analysis by encoding data values into the security model This is a compromise between the scalability if all data ow is to be kept track of the program will become prohibitively slow and complex and number of false positives I think this is a good way to give the user some control in the number of false positives Say there are a lot of errors reported but they are all caused by going down a path that is dependent on a boolean By introducing the boolean into the security model all these irrelevant errors may be eliminated while adding some complexity to the model Therefore it is up to the user to decide which false positives are too annoying to be worth getting rid of and which do not appear so often as to worth adding to the security model EECS 598 Paper Review by Kien Yue Kuo ZeroInteraction Authentication By Mark D Comer amp Brian D Noble This paper presents the ZIA system which authenticates to a laptop by using a small authentication token over a shortrange radio link This system attempts to solve the problem of the tradeoff between security and convenience for laptops ZIA differs from other systems in that it protects a laptop even when it has been physically removed By using an authentication token like a watch it requires both the token and the laptop be present in order to work Since the chance of losing both the token which is worn and the laptop is small ZIA provides an appealing solution to industries requiring the protection of security sensitive data even in the case of a stolen laptop ZIA protects from attacks involving physical possession of the laptop or proximity to it It encrypts all the data in the laptop and decrypts them only when the authorized token is available Additional method like binding the token with the laptop is used to ensure that the token is not used to authorize unintended laptops The wireless link between the token and the laptop is secured by encryption Since the wireless communication between the laptop and the token is encrypted the key must be stored somewhere and the laptop s private key may become vulnerable in case of theft The paper suggested the use of tamperresistant hardware in making the extraction difficult but there is no way to guarantee that the key cannot be extracted In case of a laptop the the worst must be assumed and the binding must be removed as suggested in the paper However this brings up another potential problem about binding To avoid frustration of the user bindings are reset infrequently and there may be a problem if someone steals the laptop unnoticed and stays within range of the token There will be a relatively large window for the thief to get data from the laptop One situation that ZIA might be vulnerable is that say a doctor is treating a patient in a serious condition and someone steals the laptop without the doctor noticing then goes into the next room and starts operating on the computer Of course this is assuming that the wireless link between the watch and the laptop is strong enough to pass through a wall In this case it is similar to having the doctor walk away from the computer and returning in the perspective of the laptop and the token so there would not be a need to bind the laptop to the token again at least not until the timeout for binding which is in the order of once a day in the paper This is more a problem on the hardware side though and if a really weak radio link is used this problem will go away however that will mean that the computer will not recognize the user returning until the user is basically right in front of the computer The time to decrypt the data and return them to a usable state is around six seconds as mentioned in the paper this may pose a minor annoyance to the user but this is still better than typing password every time the user returns EECS 598 Paper Review by Kien Yue Kuo Checking System Rules Using SystemSpeci c ProgrammerWritten Compiler Extensions By Dawnson Engler et al This paper introduces the idea of using metalevel compilation MC to write compiler extensions that automatically check code for rule violations The authors did some testing using MC on real systems like Linux and OpenBSD and found quite an impressive number of errors The idea behind MC is to use static analysis in the compiler This extends the compiler and use languagebased patters to recognize operations that are to be checked implemented as a statemachine It helps to identify problems like double freeing a pointer or sleeping while holding a lock These problems are not checked by the compiler but it can be extended to warn the programmer of these errors One of the problems of using MC is the number of false positives If the false positives overwhelm the number of real errors in the code then the user will not use it This may depend on the system since some systems may use syntax that looks wrong to the compiler This means the MC must be tweaked for different systems but that is not such a big deal since that might require some work by an experience programmer but since MC code is usually about a few hundred lines only it would not take a long time to have such rules in place Metalevel compilation is a very useful tool especially in complex systems It is impossible for a human to keep all the requirements in mind and write code that conforms to all the rules Having the compiler do the checking at compile time can help to reduce the mental workload of the programmer and catch errors caused by careless mistakes that are not caught by the compiler normally One major limitations of the extension as of the paper s writing is that the checker only performs local analysis For example in checking for mutex in Linux 48 false positives are caused by that This is caused by wa1nings issued when functions exit while holding locks but these can be eliminated with global analysis However global analysis will mean that the number of states to keep track of will be way larger since branching in a program grows exponentially and if this is performed on a complex system the work required may be huge Also whether to use global analysis depends on how useful it is If most analysis can be done locally and only a few lnction calls require global analysis it may not be worth the effort Adding this functionality will be nice and if should be left as an option for the user to choose whether or not to use it Metalevel compilation is a good idea and it may be bene cial for future compilers to integrate this functionality since currently it is dynamically linked into their own compiler xg It may improve performance since some internal data of the compiler when compiling the code can be used for the benefit of the extension
Are you sure you want to buy this material for
You're already Subscribed!
Looks like you've already subscribed to StudySoup, you won't need to purchase another subscription to get this material. To access this material simply click 'View Full Document'