SECURE WEB APPLICATIONS VIA AUTOMATIC PARTITIONINGINTRODUCTIONMain hypothesesSecurity ModelOverall OrganizationARCHITECTUREJif source codeWebIL Intermediate CodeWebIL OptimizationSplitting CodeJavaScript OutputPartitioning and ReplicationWRITING SWIFT APPLICATIONSLabels and PrincipalsSlide 15Security ConditionsImplicit Information FlowsBuilt-in principalsAn example (I)An example (II)First problemSecond problemCommentsEvaluationPerformanceConclusionSECURE WEB APPLICATIONSVIA AUTOMATIC PARTITIONINGS. Chong, J. Liu, A. C. Myers, X. Qi, K. Vikram, L. Zheng, X. ZhengCornell UniversityINTRODUCTION•Designers of web applications–Want to push as much as possible application functionality into the clients –Must protect application integrity against rogue clients•Paper presents a “principled approach” to building secure web applications–“Secure by construction”Main hypotheses•Servers can be trusted•Clients cannot–We cannot update ourselves the balances of our bank accountsSecurity Model•Swift enforces security by controlling information flow–Prevents release of information toless secure consumers–Will not accept information fromless trusted sourcesOverall Organization•Applications are written in a higher-level programming language that details all security requirements as annotations•Compiler uses these annotations to decide whether an application and its data can run on the client–Partitions code and data at the level of individual expressions and object fieldsARCHITECTUREJif source code•Written in an extension of Jif 3.0 programming language•Jif is itself an extension of Java with specific mechanisms for information flow control and access control–Expressed in Jif as labels attached to program variablesWebIL Intermediate Code•Intermediate language with much simpler annotations–S means annotated code/data must be placed on the server–S?C means annotated code/data must be placed on the server but can be replicated on the clientWebIL Optimization•Second phase produces exact placement and replication of code and data–Satisfying all security requirements–Minimizing costs and avoiding unnecessary network messagesSplitting Code•Fine grain transformation–Some statements within a specific method may run on the client while other statements must remain on the serverJavaScript Output•Jif/WebIL generate Java code to run on the client•Converted to JavaScript using the Google web toolkit•Final code uses an Ajax approach Ajax web applications can retrieve data from the server by issuing their own HTTP requestsPartitioning and Replication•Can have same computations running simultaneously on the server and the client to improve responsiveness and security•Has been done manually often using different languages–Can introduce inconsistencies•Swift replicates a single piece of codeWRITING SWIFT APPLICATIONSLabels and Principals•int {alice → alice, bob; bob ← alice} y;–Describes two policies that apply to y•alice → alice, bobmeans that alice restricts release of information to herself and bob• bob ← alicebob trusts the information and believes only alice should modify itLabels and Principals•int {alice → alice, bob; bob ← alice} y;int {bob → bob} x;int {alice → bob; bob ← alice} z;if (x == 0) { z = y};–Which conditions would make this code secure?–Let us consider the flow of information from y to zSecurity Conditions•For every confidentiality policy on y,there is one at least as restrictive on z –True for the example• For every integrity policy on z, there is one at least as restrictive on y –True for the example•Must also consider implicit flows of dataImplicit Information Flows•As in– if (x == 0) { z = …};•For the code to be secure , the security policy of z should be at least as restrictive as that of x–No true in example as the security policy of z is not as restrictive as that of x–Must add that bob trusts alice completely(“alice acts for bob”)Built-in principals•* :–The server–Maximally trusted principal in the system•Client:–Trusts the server completely:* acts for clientAn example (I)•Game makeGuess:–Client must guess a secret number between 1 and 10 in less than maxtries tries–Secret number must remain secret until the game ends–Variable counting the number of tries is not secret but should not be modified by clientAn example (II)•Variable secret is declaredint {* → *,* ← *}secret;–Secret –Only the server can update it•Variable tries is declaredint {* → client,* ← *}tries;–Not secret –Only the server can update itFirst problem•Each guess is proposed by the client–Cannot be trusted–Must be passed to the server to be compared by server to secret value•Swift has an endorse operationendorse( i, {* ← client} to {* ← *})–Raises the trust granted to some informationSecond problem•Value of secret number–Must remain secret until the client guesses it–Correct guess results in an implicit transfer of information to client•Swift has an declassify operationdeclassify({* → *} to {* → client})–Lowers the secrecy level assigned to some informationComments•Endorse and declassify operations are inherently dangerous–Must always be explicit•Swift controls their use by requiring that they occur in code marked as trusted by the affected principalEvaluation•Swift compiler adds 36,000 lines of “real” code to the Jif compiler•Server and client runtime systems are 3,000-line long each•Porting the Jif runtime system into WebIL resulted into 2,800 lines of codePerformance •Number of roundtrips is critical factor:–Still higher number than optimum–System is not fully optimizedConclusion•Swift achieves its three important goals of–Enforcement of information security–Responsive user interface–Uniform general-purpose programming modelExperience will tell how easy it will be to specify the correct labels of each variablein real