cloud9_root/src/cloud9/lib/Core/CacheSideChannel.cpp
/**
 * Solve all constraints to get models of secret keys. Each solution is a model for the secret key.
 * The observational constraint is added first (e.g. count-based or seq-based) and the solver is
 * called iteratively
 */
Solve all constraints to get models of secret keys. Each solution is a model for the secret key.
The observational constraint is added first  and the solver is
called iteratively
Solve all constraints to get models of secret keys . Each solution is a model for the secret key . The observational constraint is added first and the solver is called iteratively
int CacheChannel::solveAllConstraints(ExecutionState& state, TimingSolver* solver, ref<Expr>& obsCnstr, long bound) {
	ExecutionState cState(state);
	cState.addConstraint(obsCnstr);
	int nsolution = 0;
	{
		std::vector<std::vector<unsigned char> > values;
		std::vector<const Array*> objects;
		for (unsigned SI = 0; SI != state.symbolics.size(); SI++) {
			llvm::errs() << "\n\n -> encountered symbolic object \"" << state.symbolics[SI].first->name << "\"\n";
			llvm::errs() << "address = " << state.symbolics[SI].first->address << "\n";
			objects.push_back(state.symbolics[SI].second);
		}
		bool success = true;
		while (success) {
			success = solver->getInitialValues(data::SIDE_CHANNEL_ANALYSIS, cState, objects, values);
			solver->setTimeout(0);
			if (!success) {
				fprintf(stdout, "\n\n..... observation constraint have no possible solutions .....\n\n");
			} else {
				fprintf(stdout, "\n\n..... printing one solution for observation constraint .....\n\n");
				for (unsigned SI = 0; SI < state.symbolics.size(); SI++) {
					llvm::errs() << state.symbolics[SI].first->name << " = ";
					llvm::errs() << "(size " << state.symbolics[SI].second->size << ", little-endian) ";
					for (unsigned II = 0; II < values[SI].size(); II++)
						fprintf(stdout, "%d ", values[SI][II]);
					fprintf(stdout, "\n");
					fflush(stdout);
				}
				nsolution++;
				fprintf(stdout, "..... #keys discovered so far = %d .....\n\n", nsolution);
				if (nsolution >= bound) break;
				naiveCEGAR(state, cState, values);
			}
		}
	}
	return nsolution;
}
int CacheChannel :: solveAllConstraints ( ExecutionState & state , TimingSolver * solver , ref < Expr > & obsCnstr , long bound ) { ExecutionState cState ( state ) ; cState . addConstraint ( obsCnstr ) ; int nsolution = 0 ; { std :: vector < std :: vector < unsigned char > > values ; std :: vector < const Array * > objects ; for ( unsigned SI = 0 ; SI != state . symbolics . size ( ) ; SI ++ ) { llvm :: errs ( ) << " \n \n \" " << state . symbolics [ SI ] . first -> name << " \" \n " ; llvm :: errs ( ) << " " << state . symbolics [ SI ] . first -> address << " \n " ; objects . push_back ( state . symbolics [ SI ] . second ) ; } bool success = true ; while ( success ) { success = solver -> getInitialValues ( data :: SIDE_CHANNEL_ANALYSIS , cState , objects , values ) ; solver -> setTimeout ( 0 ) ; if ( ! success ) { fprintf ( stdout , " \n \n \n \n " ) ; } else { fprintf ( stdout , " \n \n \n \n " ) ; for ( unsigned SI = 0 ; SI < state . symbolics . size ( ) ; SI ++ ) { llvm :: errs ( ) << state . symbolics [ SI ] . first -> name << " " ; llvm :: errs ( ) << " " << state . symbolics [ SI ] . second -> size << " " ; for ( unsigned II = 0 ; II < values [ SI ] . size ( ) ; II ++ ) fprintf ( stdout , " " , values [ SI ] [ II ] ) ; fprintf ( stdout , " \n " ) ; fflush ( stdout ) ; } nsolution ++ ; fprintf ( stdout , " \n \n " , nsolution ) ; if ( nsolution >= bound ) break ; naiveCEGAR ( state , cState , values ) ; } } } return nsolution ; }
Solve all constraints to get models of secret keys.
Solve all constraints to get models of secret keys .
// add the observational constraint // get the models for cache miss constraints // get values of symbolic objects /********** the KEY CEGAR loop to get different solutions for a given cache miss **********/ /* get a model (solution) for the observed cache misses */ /* no solution exists */ /* we have a solution for observed cache misses */ //ExprPPrinter::printQuery(llvm::errs(), cState.constraints, //                    	ConstantExpr::alloc(0, Expr::Bool)); /* sudiptac: only get as many as "bound" solutions */ /* implement features to get a different solution each time
				 * "getInitialValues" is called	*/ /********** END of KEY CEGAR loop **********/